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/regress0 | |
| 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/regress0')
| -rw-r--r-- | test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 | 2 |
1 files changed, 0 insertions, 2 deletions
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) |