Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-08-28 | fixing bug580 caused by bad bv inequality explanation | lianah | |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof ↵ | Morgan Deters | |
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 | |||
2013-09-18 | Support a personal build configuration and make rules. | Morgan Deters | |
2013-05-07 | fix for bug500 | Dejan Jovanović | |
2013-02-26 | Merge branch '1.0.x' | lianah | |
2013-02-26 | fix for bv crash in incremental mode; this is a temporary fix for bug 493 | lianah | |
2013-01-28 | some fixes for win32, including ability to "make check" win32 builds via wine | Morgan Deters | |
2012-11-17 | Fixed last currently known bug in array models | Clark Barrett | |
2012-11-16 | Fix for bug451 | Clark Barrett | |
2012-11-15 | fuzz15 should have been fuzz14 | Clark Barrett | |
2012-11-15 | Fixed another AUFBV model bug. BV equality subtheory needed to do something | Clark Barrett | |
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. | |||
2012-11-14 | bug fixes to models, array rewriter with previously failing testcases | Clark Barrett | |
2012-11-13 | Fixed an array rewriting bug found by fuzzer | Clark Barrett | |
2012-11-13 | Testcases for fixed bugs | Clark Barrett | |
2012-11-10 | Fixed missing \ in uflra/Makefile.ma | Clark Barrett | |
Fixed another model bug and added previously failing fuzz testcase | |||
2012-08-28 | fix regression tests for automake 1.11 and automake 1.12---both versions ↵ | Morgan Deters | |
should work now | |||
2012-06-28 | Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2 | Clark Barrett | |
2012-06-17 | fixing wrong assertion | Dejan Jovanović | |
2012-06-16 | changing theoryOf in shared mode with arrays to move equalities to arrays | Dejan Jovanović | |
disabled in bitvectors due to non-stably infinite problems the option to enable it is --theoryof-mode=term | |||
2012-06-15 | Fixes some assertion failures | Clark Barrett | |
2012-06-14 | fixing the problems with the bvminisat. there was a case when things would ↵ | Dejan Jovanović | |
get bitblasted, it would restart to add the clauses, and loose propagation information. | |||
2012-06-14 | fixes for the hasTerm issues in the shared database under the decision heuristic | Dejan Jovanović | |
2012-06-14 | This commit: | Kshitij Bansal | |
* 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 | |||
2012-06-14 | * removing rewriteEquality from the rewriter | Dejan Jovanović | |
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized | |||
2012-06-13 | enabling regressions from last night, all fixed | Dejan Jovanović | |
2012-06-13 | r2.node == response.node failure | Dejan Jovanović | |
2012-06-12 | missing problems | Dejan Jovanović | |
2012-06-12 | bufixes and the bugs | Dejan Jovanović | |
* array now only propagates thropugh the equality engine * assertions in the equality rewriting to ensure eq -> { eq, T, F } | |||
2012-06-12 | more breakage in aufbv | Dejan Jovanović | |
Assertion `value(l) == (lbool((uint8_t)0))' failed. and d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end() | |||
2012-06-12 | tests for the | Dejan Jovanović | |
!isEliminated(var(ps[i])) assert fails | |||
2012-06-11 | some failing examples | Dejan Jovanović | |
2012-06-10 | adding an assertion to trigger the problem of bug349 and the testcase | Dejan Jovanović | |
bv rewriter apparently deosn't have a proper normal form for equalities | |||
2012-06-10 | fixes for bug347 | Dejan Jovanović | |
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 | |||
2012-06-07 | fixing the wrong results. arrays equality adaptor had a missing case when ↵ | Dejan Jovanović | |
propagating disequalities between shared terms. | |||
2012-06-07 | cleaning up the expample for the future | Dejan Jovanović | |
2012-06-07 | Added small test case for diseq propagation | Clark Barrett | |
2012-06-07 | fixing some bugs in propagation of disequalities | Dejan Jovanović | |
still doesnt fix the wrong answers thought :( | |||
2012-06-06 | Fixing numerous issues with tests and "make dist": | Morgan Deters | |
* 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.) | |||
2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ↵ | Dejan Jovanović | |
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 | |||
2012-05-17 | Fixed bug 338: | Liana Hadarean | |
- fixed buggy rewrite rules assuming certain nodes only had 2 children - added support for bv-rewrite dump - fixed smt2_printer for bv constants | |||
2012-05-08 | Merging in bvprop branch, with proper bit-vector propagation. | Liana Hadarean | |
This should also fix bug 325. | |||
2012-04-18 | add the missing BINARY variable in some test/regress makefiles | Kshitij Bansal | |
2012-04-11 | merge from arrays-clark branch | Morgan Deters | |