diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-19 20:54:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-19 20:54:40 -0500 |
| commit | 7dfd55085c60affdc4523c330ea2d2daa69ae66a (patch) | |
| tree | 834a1b51dfbee612da15f194b7ed8d88003e7144 /src/theory/quantifiers/sygus/synth_engine.cpp | |
| parent | 96b6b3a172d76753355e258edadcf977b39edcb8 (diff) | |
Sygus abduction feature (#2744)
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index d3eff1750..0623c257a 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -159,6 +159,7 @@ void SynthEngine::assignConjecture(Node q) { // create new smt engine to do quantifier elimination SmtEngine smt_qe(nm->toExprManager()); + smt_qe.setIsInternalSubsolver(); smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo()); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." |