diff options
Diffstat (limited to 'test/regress')
| -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 |