diff options
Diffstat (limited to 'src/preprocessing')
| -rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 78e9e639a..471d68ff8 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -256,10 +256,11 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions, // quantify the body Trace("sygus-infer") << "Make inner sygus conjecture..." << std::endl; + body = body.negate(); if (!qvars.empty()) { Node bvl = nm->mkNode(BOUND_VAR_LIST, qvars); - body = nm->mkNode(EXISTS, bvl, body.negate()); + body = nm->mkNode(EXISTS, bvl, body); } // sygus attribute to mark the conjecture as a sygus conjecture |