summaryrefslogtreecommitdiff
path: root/src/preprocessing/passes
diff options
context:
space:
mode:
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r--src/preprocessing/passes/global_negate.cpp10
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback