diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-11 01:30:37 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-11 01:30:37 +0000 |
| commit | a7f004fad9947f3a953dbd6d14838f1e04f105eb (patch) | |
| tree | 05da12b483a2e78f0bb3bb103cc49b6a5cabd648 /test | |
| parent | 3908dc0247d9cffa67f87294374bbd10a797b1e5 (diff) | |
Fix for the main bug that was bugging me -- Bug 49. The assertions queue in the theories didn't get cleared on SatSolver backtracking so there were unasserted literals being returned as part of some conflicts. Sat solver now explicitely calls in the theory engine after it backtracks in order to clear the queues (clearAssertionQueues).
Also, changed the let.smt as it used to exibit "single literal conflict" problem. The sat solve can not except conflicts similar to (x != x), these should be rewritten to false during pre-processing.
Adding 3 more small problems from the library that we can solve now to the regressions.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/let.smt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/uf/Makefile.am | 5 |
2 files changed, 6 insertions, 2 deletions
diff --git a/test/regress/regress0/let.smt b/test/regress/regress0/let.smt index 45d0eaecb..8b747c3e1 100644 --- a/test/regress/regress0/let.smt +++ b/test/regress/regress0/let.smt @@ -2,4 +2,5 @@ :logic QF_UF :status unsat :extrafuns ((a U) (b U) (f U U)) - :formula (let (?x a) (not (= ?x a))))
\ No newline at end of file + :formula (let (?x a) (and (= a b) (not (= ?x b)))) +)
\ No newline at end of file diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index fa298f1a5..a4e08ff99 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -2,7 +2,10 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4 TESTS = simple.01.cvc \ simple.02.cvc \ simple.03.cvc \ - simple.04.cvc + simple.04.cvc \ + dead_dnd002.smt \ + iso_brn001.smt \ + SEQ032_size2.smt # synonyms for "check" .PHONY: regress regress0 test |