projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3d1c710) | patch
fixes for bug347
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Sun, 10 Jun 2012 03:03:17 +0000 (03:03 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Sun, 10 Jun 2012 03:03:17 +0000 (03:03 +0000)
commite761ec344a7c9d9b5bff5f312cdb8932083e0bc8
tree8a936c4e0c22cf45ec33d6f87a7bc01f31ab49cdtree
parent3d1c71026c7b8aaa2e9689d27415d80c412ece2ecommit | 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
src/theory/arith/congruence_manager.h diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history
src/theory/bv/bv_subtheory_eq.cpp diff | blob | history
src/theory/bv/bv_subtheory_eq.h diff | blob | history
src/theory/shared_terms_database.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history
src/theory/uf/equality_engine.h diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history
test/regress/regress0/aufbv/Makefile.am diff | blob | history
test/regress/regress0/aufbv/bug347.smt [new file with mode: 0644] blob