diff options
| -rw-r--r-- | src/options/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 25 |
2 files changed, 14 insertions, 12 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 457fd23cd..236d2bc6a 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -21,6 +21,7 @@ libcvc4_add_sources( language.h open_ostream.cpp open_ostream.h + option_exception.cpp option_exception.h options.h options_handler.cpp diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a41108a71..84e7f3e23 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -155,6 +155,8 @@ set(regress_0_tests regress0/bug605.cvc regress0/bug639.smt2 regress0/buggy-ite.smt2 + regress0/bv/ackermann1.smt2 + regress0/bv/ackermann2.smt2 regress0/bv/bool-to-bv.smt2 regress0/bv/bug260a.smt regress0/bv/bug260b.smt @@ -340,6 +342,7 @@ set(regress_0_tests regress0/datatypes/cdt-non-canon-stream.smt2 regress0/datatypes/coda_simp_model.smt2 regress0/datatypes/conqueue-dt-enum-iloop.smt2 + regress0/datatypes/data-nested-codata.smt2 regress0/datatypes/datatype.cvc regress0/datatypes/datatype0.cvc regress0/datatypes/datatype1.cvc @@ -434,8 +437,10 @@ set(regress_0_tests regress0/fmf/quant_real_univ.cvc regress0/fmf/sat-logic.smt2 regress0/fmf/sc_bad_model_1221.smt2 + regress0/fmf/sort-infer-typed-082718.smt2 regress0/fmf/syn002-si-real-int.smt2 regress0/fmf/tail_rec.smt2 + regress0/fp/ext-rew-test.smt2 regress0/fp/simple.smt2 regress0/fuzz_1.smt regress0/fuzz_3.smt @@ -496,9 +501,11 @@ set(regress_0_tests regress0/logops.05.cvc regress0/model-core.smt2 regress0/nl/coeff-sat.smt2 + regress0/nl/ext-rew-aggr-test.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 regress0/nl/nia-wrong-tl.smt2 + regress0/nl/nlExtPurify-test.smt2 regress0/nl/nta/cos-sig-value.smt2 regress0/nl/nta/exp-n0.5-lb.smt2 regress0/nl/nta/exp-n0.5-ub.smt2 @@ -512,6 +519,7 @@ set(regress_0_tests regress0/nl/subs0-unsat-confirm.smt2 regress0/nl/very-easy-sat.smt2 regress0/nl/very-simple-unsat.smt2 + regress0/options/invalid_dump.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/constraint.smt2 @@ -616,6 +624,7 @@ set(regress_0_tests regress0/quantifiers/issue1805.smt2 regress0/quantifiers/issue2031-bv-var-elim.smt2 regress0/quantifiers/issue2033-macro-arith.smt2 + regress0/quantifiers/issue2035.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macros-int-real.smt2 regress0/quantifiers/macros-real-arg.smt2 @@ -791,6 +800,7 @@ set(regress_0_tests regress0/simplification_bug2.smt regress0/smallcnf.cvc regress0/smt2output.smt2 + regress0/smtlib/get-unsat-assumptions.smt2 regress0/strings/bug001.smt2 regress0/strings/bug002.smt2 regress0/strings/bug612.smt2 @@ -811,12 +821,14 @@ set(regress_0_tests regress0/strings/norn-31.smt2 regress0/strings/norn-simp-rew.smt2 regress0/strings/repl-rewrites2.smt2 + regress0/strings/rewrites-re-concat.smt2 regress0/strings/rewrites-v2.smt2 regress0/strings/std2.6.1.smt2 regress0/strings/stoi-solve.smt2 regress0/strings/str003.smt2 regress0/strings/str004.smt2 regress0/strings/str005.smt2 + regress0/strings/str_unsound_ext_rew_eq.smt2 regress0/strings/strings-charat.cvc regress0/strings/strings-native-simple.cvc regress0/strings/strip-endpoint-itos.smt2 @@ -830,6 +842,7 @@ set(regress_0_tests regress0/sygus/check-generic-red.sy regress0/sygus/const-var-test.sy regress0/sygus/dt-no-syntax.sy + regress0/sygus/hd-05-d1-prog-nogrammar.sy regress0/sygus/inv-different-var-order.sy regress0/sygus/let-ringer.sy regress0/sygus/let-simp.sy @@ -1000,18 +1013,6 @@ set(regress_0_tests regress0/wiki.19.cvc regress0/wiki.20.cvc regress0/wiki.21.cvc - regress0/bv/ackermann1.smt2 - regress0/bv/ackermann2.smt2 - regress0/datatypes/data-nested-codata.smt2 - regress0/fmf/sort-infer-typed-082718.smt2 - regress0/fp/ext-rew-test.smt2 - regress0/nl/ext-rew-aggr-test.smt2 - regress0/nl/nlExtPurify-test.smt2 - regress0/quantifiers/issue2035.smt2 - regress0/smtlib/get-unsat-assumptions.smt2 - regress0/strings/rewrites-re-concat.smt2 - regress0/strings/str_unsound_ext_rew_eq.smt2 - regress0/sygus/hd-05-d1-prog-nogrammar.sy ) #-----------------------------------------------------------------------------# |