diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-10 23:31:29 -0500 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-09-10 23:31:29 -0500 |
commit | b0c630be79034d898e473c167a16fb61c380b733 (patch) | |
tree | bd5913e96365080e300e6eb9792a77b8d6af831d /src/preprocessing | |
parent | 945da3af1ea94aeabcd8f39b23a8741c6e41c358 (diff) |
Fix global negate (#2449)
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/global_negate.cpp | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index ddebf961f..ae71b3e78 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -105,9 +105,15 @@ PreprocessingPassResult GlobalNegate::applyInternal( Node trueNode = nm->mkConst(true); for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { - assertionsToPreprocess->replace(i, trueNode); + if (i == 0) + { + assertionsToPreprocess->replace(i, simplifiedNode); + } + else + { + assertionsToPreprocess->replace(i, trueNode); + } } - assertionsToPreprocess->push_back(simplifiedNode); return PreprocessingPassResult::NO_CONFLICT; } |