summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/theory_arith.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index eb0c99abe..e4284286e 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1104,7 +1104,8 @@ Constraint TheoryArith::constraintFromFactQueue(){
Assert(!isSetup(eq));
Node reEq = Rewriter::rewrite(eq);
if(reEq.getKind() == CONST_BOOLEAN){
- if(reEq.getConst<bool>() != isDistinct){
+ if(reEq.getConst<bool>() == isDistinct){
+ // if is (not true), or false
Assert((reEq.getConst<bool>() && isDistinct) ||
(!reEq.getConst<bool>() && !isDistinct));
d_raiseConflict(assertion);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback