projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6790328) | patch
fixing some bugs in propagation of disequalities
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 7 Jun 2012 07:11:24 +0000 (07:11 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 7 Jun 2012 07:11:24 +0000 (07:11 +0000)
commit49dd14da8d872403b4d772a2d49224e4d6bda227
tree5abbd246c8a1bb797e97d4b9754a4f850e1dc1b5tree
parent67903280f8fe6946a36ef9fc08bfc747f74bfbd7commit | diff
fixing some bugs in propagation of disequalities
still doesnt fix the wrong answers thought :(
13 files changed:
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/theory.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
test/regress/regress0/aufbv/dubreva005ue.delta01.smt [new file with mode: 0644] blob
test/regress/regress0/aufbv/dubreva005ue.smt [new file with mode: 0644] blob
test/regress/regress0/uflia/diseqprop.01.smt [new file with mode: 0644] blob
test/regress/regress0/uflia/diseqprop.02.smt [new file with mode: 0644] blob
test/regress/regress0/uflia/diseqprop.03.smt [new file with mode: 0644] blob
test/regress/regress0/uflia/diseqprop.04.smt [new file with mode: 0644] blob
test/regress/regress0/uflia/diseqprop.05.smt [new file with mode: 0644] blob
test/regress/regress0/uflia/diseqprop.06.smt [new file with mode: 0644] blob