diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-29 11:11:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-29 16:11:05 +0000 |
| commit | b685ed411b6814f0810ce8f61d07aa49bd75ea3b (patch) | |
| tree | 75029fdd0b7b8d82f6296047c10818cb745c9cdb /test/regress/CMakeLists.txt | |
| parent | f2672e53fae29abe40fc69b004d1df5be0ce1e8b (diff) | |
Integrate central equality engine approach into theory engine, add option and regressions (#6943)
This commit makes TheoryEngine take into account whether theories are using the central equality engine.
With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 151e01088..902037088 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -120,6 +120,7 @@ set(regress_0_tests regress0/aufbv/bug493.smtv1.smt2 regress0/aufbv/bug509.smtv1.smt2 regress0/aufbv/bug580.delta.smt2 + regress0/aufbv/cee-small-shared-eq.smt2 regress0/aufbv/diseqprop.01.smtv1.smt2 regress0/aufbv/dubreva005ue.delta01.smtv1.smt2 regress0/aufbv/fifo32bc06k08.delta01.smtv1.smt2 @@ -468,6 +469,7 @@ set(regress_0_tests regress0/datatypes/bug597-rbt.smt2 regress0/datatypes/bug604.smt2 regress0/datatypes/bug625.smt2 + regress0/datatypes/canExp-dtPendingMerge.smt2 regress0/datatypes/cdt-model-cade15.smt2 regress0/datatypes/cdt-non-canon-stream.smt2 regress0/datatypes/coda_simp_model.smt2 @@ -1084,6 +1086,7 @@ set(regress_0_tests regress0/sets/pre-proc-univ.smt2 regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 regress0/sets/setel-eq.smt2 + regress0/sets/sets-deq-dd.smt2 regress0/sets/sets-equal.smt2 regress0/sets/sets-extr.smt2 regress0/sets/sets-inter.smt2 @@ -1542,10 +1545,12 @@ set(regress_1_tests regress1/bv/test-bv-abstraction.smt2 regress1/bv/unsound1.smt2 regress1/bvdiv2.smt2 + regress1/cee-bug0909-dd-scope.smt2 regress1/constarr3.cvc regress1/constarr3.smt2 regress1/cores/issue5604.smt2 regress1/datatypes/acyclicity-sr-ground096.smt2 + regress1/datatypes/cee-prs-small-dd2.smt2 regress1/datatypes/dt-color-2.6.smt2 regress1/datatypes/dt-param-card4-unsat.smt2 regress1/datatypes/error.cvc @@ -1734,6 +1739,7 @@ set(regress_1_tests regress1/push-pop/arith_lra_02.smt2 regress1/push-pop/bug-fmf-fun-skolem.smt2 regress1/push-pop/bug216.smt2 + regress1/push-pop/cee-prs-small.smt2 regress1/push-pop/fuzz_1.smt2 regress1/push-pop/fuzz_10.smt2 regress1/push-pop/fuzz_11.smt2 @@ -1813,6 +1819,8 @@ set(regress_1_tests regress1/quantifiers/burns13.smt2 regress1/quantifiers/burns4.smt2 regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 + regress1/quantifiers/cee-npnt-dd.smt2 + regress1/quantifiers/cee-os-delta.smt2 regress1/quantifiers/cdt-0208-to.smt2 regress1/quantifiers/const.cvc regress1/quantifiers/constfunc.cvc @@ -2088,6 +2096,7 @@ set(regress_1_tests regress1/strings/bug686dd.smt2 regress1/strings/bug768.smt2 regress1/strings/bug799-min.smt2 + regress1/strings/cee-norn-aes-trivially.smt2 regress1/strings/chapman150408.smt2 regress1/strings/cmu-2db2-extf-reg.smt2 regress1/strings/cmu-5042-0707-2.smt2 @@ -2482,6 +2491,7 @@ set(regress_2_tests regress2/piVC_5581bd.smt2 regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 + regress2/quantifiers/cee-event-wrong-sat.smt2 regress2/quantifiers/gn-wrong-091018.smt2 regress2/quantifiers/issue3481-unsat1.smt2 regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 @@ -2722,6 +2732,7 @@ set(regression_disabled_tests # previously sygus inference did not apply, now (correctly) times out regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 + regress2/quantifiers/exp-trivially-dd3.smt2 regress2/nl/dumortier-050317.smt2 # timeout on some builds after changes to justification heuristic regress2/nl/nt-lemmas-bad.smt2 |