diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-11-20 16:42:58 -0300 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-20 13:42:58 -0600 |
| commit | 596fe8c79106dd9b7764df2ddce6b2d3344fea34 (patch) | |
| tree | 194dedc76376b7023cbd431289e4724bbbb98e3d /src/theory/quantifiers/sygus/synth_conjecture.cpp | |
| parent | 45bcf28ab55c0fe471b445820fc21627495beee8 (diff) | |
Lazy evaluation via rec-funs of ITE expressions (#3482)
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 6e69715ef..6591e6828 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -591,7 +591,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) Trace("cegqi-debug") << "...squery : " << squery << std::endl; squery = Rewriter::rewrite(squery); Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; - Assert(squery.isConst() && squery.getConst<bool>()); + Assert(options::sygusRecFun() + || (squery.isConst() && squery.getConst<bool>())); #endif return false; } |