diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-20 17:18:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-20 17:18:02 -0500 |
| commit | b967cc5c8d84023c1b821c59b7bca736ffda6bed (patch) | |
| tree | b1900e3817888a0ff321d70da4a31796db82b0ee /src/preprocessing | |
| parent | 16c2fe5ec2ebb29da131aa590a4a0b79b1e94dc9 (diff) | |
Fixes for sygus inference on quantifier free problems (#3202)
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 |