Age | Commit message (Collapse) | Author |
|
Fixed another model bug and added previously failing fuzz testcase
|
|
should work now
|
|
|
|
|
|
disabled in bitvectors due to non-stably infinite problems
the option to enable it is --theoryof-mode=term
|
|
|
|
get bitblasted, it would restart to add the clauses, and loose propagation information.
|
|
|
|
* enables decision heuristic (justification) for QF_BV and QF_AUFBV
* disables a failing regression in aufbv (because of equality engine
assert failure trigerred by above change)
* moves around the init procedure smt_engine
* destruction time issues because of moving this -- still to be fixed,
currently get around by not destucting stuff in driver
|
|
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
|
|
|
|
|
|
|
|
* array now only propagates thropugh the equality engine
* assertions in the equality rewriting to ensure eq -> { eq, T, F }
|
|
Assertion `value(l) == (lbool((uint8_t)0))' failed.
and
d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end()
|
|
!isEliminated(var(ps[i]))
assert fails
|
|
|
|
bv rewriter apparently deosn't have a proper normal form for equalities
|
|
it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately
|
|
propagating disequalities between shared terms.
|
|
|
|
|
|
still doesnt fix the wrong answers thought :(
|
|
* test/regress/regress0/unconstrained wasn't being distributed. This caused the debian build failure last night. (It still doesn't run on "make check", but had to be distributed properly.)
* Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format. (Told automake to use a newer tar format.)
|
|
are still the AUFBV wrong results, but it seems better.
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
|
|
- fixed buggy rewrite rules assuming certain nodes only had 2 children
- added support for bv-rewrite dump
- fixed smt2_printer for bv constants
|
|
This should also fix bug 325.
|
|
|
|
|