projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e568f34) | patch
fixing the wrong results. arrays equality adaptor had a missing case when propagating...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 7 Jun 2012 22:19:53 +0000 (22:19 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 7 Jun 2012 22:19:53 +0000 (22:19 +0000)
commit01002e4b876c53661aaa2f3b3df9680e1d8e98d7
tree96217e239b5067e92174fe3ef8e74360177f794btree
parente568f34e1f4713c678336fbef1006e585128d466commit | diff
fixing the wrong results. arrays equality adaptor had a missing case when propagating disequalities between shared terms.
src/theory/arrays/theory_arrays.h diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history
src/theory/uf/equality_engine.h diff | blob | history
test/regress/regress0/aufbv/Makefile.am diff | blob | history