git.libre-soc.org Git - cvc5.git/commit

author	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Mon, 11 Jun 2012 18:54:38 +0000 (18:54 +0000)
committer	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Mon, 11 Jun 2012 18:54:38 +0000 (18:54 +0000)
commit	d54c761087af01874ea6674111888cb94ffa4ee6
tree	2f196940df9b488a1298ccfdee9bf1b54a70ccac	tree
parent	e148b0a99917b21499b2f596aa22403559baf677	commit \| diff

fixing bitvector bugs
* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally

52 files changed:

src/prop/bvminisat/core/Solver.cc		diff \| blob \| history
src/theory/bv/bitblaster.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory.h		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_eq.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
test/regress/regress0/bv/Makefile.am		diff \| blob \| history
test/regress/regress0/bv/core/Makefile.am		diff \| blob \| history
test/regress/regress0/bv/fuzz15.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz16.delta01.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz17.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz18.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz18.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz19.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz19.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz20.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz20.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz21.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz21.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz22.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz22.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz23.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz23.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz24.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz24.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz25.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz25.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz26.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz26.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz27.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz27.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz28.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz28.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz29.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz29.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz30.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz30.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz31.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz31.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz32.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz32.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz33.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz33.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz34.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz34.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz35.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz35.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz36.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz36.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz37.delta01.smt		diff \| blob \| history
test/regress/regress0/bv/fuzz37.smt		diff \| blob \| history

RSS Atom