projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a648adc) | patch
fixing the problems with the bvminisat. there was a case when things would get bitbla...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 14 Jun 2012 22:20:15 +0000 (22:20 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Thu, 14 Jun 2012 22:20:15 +0000 (22:20 +0000)
commit761bb503aa475fae1748afd6f583dd9af772f1cd
treed899a63d6288ed606898b960b2b3ced8bc4a9e54tree
parenta648adc7767ccd720cf1684ee8adac3d03f64f53commit | diff
fixing the problems with the bvminisat. there was a case when things would get bitblasted, it would restart to add the clauses, and loose propagation information.
13 files changed:
src/prop/bvminisat/bvminisat.cpp diff | blob | history
src/prop/bvminisat/bvminisat.h diff | blob | history
src/prop/bvminisat/core/Solver.cc diff | blob | history
src/prop/bvminisat/core/Solver.h diff | blob | history
src/prop/sat_solver.h diff | blob | history
src/theory/bv/bitblaster.cpp diff | blob | history
src/theory/bv/bitblaster.h diff | blob | history
src/theory/bv/bv_subtheory_bitblast.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
test/regress/regress0/aufbv/Makefile.am diff | blob | history
test/regress/regress0/aufbv/fuzz07.smt [new file with mode: 0644] blob
test/regress/regress0/aufbv/fuzz08.smt [new file with mode: 0644] blob
test/regress/regress0/aufbv/fuzz09.smt [new file with mode: 0644] blob