Age | Commit message (Collapse) | Author |
|
With the recent changes to the regress tests, some of the Makefiles were
not in sync anymore. This commit fixes that.
|
|
|
|
|
|
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
|
|
|
|
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
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 }
|
|
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.
|
|
* 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
|
|
|
|
|