projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0cf2cf6) | patch
Fixed another AUFBV model bug. BV equality subtheory needed to do something
authorClark Barrett <barrett@cs.nyu.edu>
Thu, 15 Nov 2012 02:14:42 +0000 (02:14 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Thu, 15 Nov 2012 02:14:42 +0000 (02:14 +0000)
commitdc0372a91ae46e6fc5ead1f51a1fe033cfd19944
treea45d1ae09a4026f516af9e68e37cab4cc76d2506tree
parent0cf2cf65658ce8128d0cc87d6a9714b5284d45c4commit | diff
Fixed another AUFBV model bug.  BV equality subtheory needed to do something
similar to arrays - limit the set of terms reported to those relevant in the
current context.  Also removed collectModelInfo from sharedTermsDatabase -
doesn't seem to be needed any more.
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history
src/theory/bv/bv_subtheory_eq.cpp diff | blob | history
src/theory/theory.cpp diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
test/regress/regress0/aufbv/Makefile.am diff | blob | history
test/regress/regress0/aufbv/fuzz15.smt [new file with mode: 0644] blob