diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-10 03:03:17 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-10 03:03:17 +0000 |
commit | e761ec344a7c9d9b5bff5f312cdb8932083e0bc8 (patch) | |
tree | 8a936c4e0c22cf45ec33d6f87a7bc01f31ab49cd /src/theory/arith | |
parent | 3d1c71026c7b8aaa2e9689d27415d80c412ece2e (diff) |
fixes for bug347
it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/congruence_manager.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 5e4616628..5f49ab3ab 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -65,12 +65,12 @@ private: } } - bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; if (t1.getKind() == kind::CONST_BOOLEAN) { - return d_acm.propagate(t1.iffNode(t2)); + d_acm.propagate(t1.iffNode(t2)); } else { - return d_acm.propagate(t1.eqNode(t2)); + d_acm.propagate(t1.eqNode(t2)); } } }; |