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/shared_terms_database.h | |
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/shared_terms_database.h')
-rw-r--r-- | src/theory/shared_terms_database.h | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 1a38d7332..fccd2e6bc 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -92,9 +92,8 @@ private: return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value); } - bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { d_sharedTerms.conflict(t1, t2, true); - return false; } }; |