summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/sygus_invariance.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_invariance.cpp')
-rw-r--r--src/theory/quantifiers/sygus/sygus_invariance.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index 54a3cce50..24b47b216 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -14,8 +14,8 @@
#include "theory/quantifiers/sygus/sygus_invariance.h"
-#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
#include "theory/quantifiers/sygus/sygus_pbe.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
using namespace CVC4::kind;
@@ -87,7 +87,7 @@ bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
}
void EquivSygusInvarianceTest::init(
- TermDbSygus* tds, TypeNode tn, CegConjecture* aconj, Node e, Node bvr)
+ TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr)
{
// compute the current examples
d_bvr = bvr;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback