diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-06 22:41:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-07 03:41:04 +0000 |
| commit | 4376ff5bd3df8dabb847d4cd99465f894230fb60 (patch) | |
| tree | d6e2b754ac973990606937af9163723ffb48125d /test/regress | |
| parent | 1eb3c6c8eb3da95cababcc0b1705c0299eee099c (diff) | |
Refactoring and fixes of set defaults for quantifiers (#7120)
This PR further refactors set defaults for incompatibility issues related to quantifiers.
It adds a new restriction that was discovered recently: --nl-rlv should not be used in quantified logics. Some regressions are modified that are impacted by this restriction.
Also does minor rearrangements to the order in which default options are set.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/nl/issue3647.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3648.smt2 | 2 |
4 files changed, 4 insertions, 5 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8804563b4..8909bfc06 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2345,7 +2345,6 @@ set(regress_1_tests regress1/sygus/issue3634.smt2 regress1/sygus/issue3635.smt2 regress1/sygus/issue3644.smt2 - regress1/sygus/issue3648.smt2 regress1/sygus/issue3649.sy regress1/sygus/issue3802-default-consts.sy regress1/sygus/issue3839-cond-rewrite.smt2 @@ -2740,6 +2739,8 @@ set(regression_disabled_tests regress1/sygus/interpol_from_pono_3.smt2 regress1/sygus/interpol_dt.smt2 regress1/sygus/inv_gen_fig8.sy + # timeout since nl-rlv is required; however it cannot be used with quantifiers + regress1/sygus/issue3648.smt2 # new reconstruct algorithm is slow at reconstructing random constants (see wishue #82) regress0/sygus/c100.sy # For the six regressions below, solution terms require rewrites not in diff --git a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 index 3aeb38c6e..95deeb141 100644 --- a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 +++ b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --nl-rlv=always --no-sygus-inst -; EXPECT: unsat (set-logic NRA) (set-info :status unsat) (declare-fun c () Real) diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2 index 6c66d2e4c..f863842de 100644 --- a/test/regress/regress1/nl/issue3647.smt2 +++ b/test/regress/regress1/nl/issue3647.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models --produce-models --decision=internal --nl-rlv=always ; EXPECT: sat -(set-logic ALL) +(set-logic QF_NRAT) (set-info :status sat) (assert (distinct (sin 1.0) 0.0)) (check-sat) diff --git a/test/regress/regress1/sygus/issue3648.smt2 b/test/regress/regress1/sygus/issue3648.smt2 index 2fc1a6115..e7b7547c4 100644 --- a/test/regress/regress1/sygus/issue3648.smt2 +++ b/test/regress/regress1/sygus/issue3648.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -; COMMAND-LINE: --sygus-inference --no-check-models --nl-rlv=always +; COMMAND-LINE: --sygus-inference --no-check-models (set-logic ALL) (declare-fun a () Real) (assert (> a 0.000001)) |