diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-08-17 22:24:26 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-08-17 22:24:26 +0000 |
commit | 08a57829cdd0ef4c02fee349b4b721d3e4a3f6d1 (patch) | |
tree | 9ea214ffb5a5a03e3c71c09814f17787be6d022b /test/regress/regress0 | |
parent | daf715e2ccb53bd88c6f374840b5d41e72c61c90 (diff) |
Merge from "cc" branch:
CongruenceClosure implementation; CongruenceClosure white-box test.
New UF theory implementation based on new CC module. This one
supports predicates. The two UF implementations exist in parallel
(they can be selected at runtime via the new command line option
"--uf").
Added type infrastructure for TUPLE.
Fixes to unit tests that failed in 16-August-2010 regressions.
Needed to instantiate TheoryEngine with an Options structure, and
explicitly call ->shutdown() on it before destruction (like the
SMTEngine does).
Fixed test makefiles to (1) perform all tests even in the presence of
failures, (2) give proper summaries of subdirectory tests
(e.g. regress0/uf and regress0/precedence)
Other minor changes.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 09dc52ce4..7f732b17f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,6 +1,7 @@ SUBDIRS = . precedence uf TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 +MAKEFLAGS = -k # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index bf516107e..452024309 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -16,9 +16,9 @@ TESTS = \ euf_simp11.smt \ euf_simp12.smt \ euf_simp13.smt \ + eq_diamond1.smt \ dead_dnd002.smt \ iso_brn001.smt \ - SEQ032_size2.smt \ simple.01.cvc \ simple.02.cvc \ simple.03.cvc \ |