diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-12-11 16:38:00 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-12-11 16:38:00 -0600 |
commit | 147fd723e6c13eb3dd44a43073be03a64ea3fe66 (patch) | |
tree | 0a6eb33068ff609262566fa744a885cf4658a934 /test/regress | |
parent | 1c114dc487d94d72ebf3453611c42b28777d6482 (diff) |
Remove alternate versions of mbqi (#2742)
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt | 2 | ||||
-rw-r--r-- | test/regress/regress0/fmf/QEpres-uf.855035.smt | 2 | ||||
-rw-r--r-- | test/regress/regress1/fmf/nlp042+1.smt2 | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt index e8c7949dc..bb2630b93 100644 --- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt +++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --mbqi=gen-ev +; COMMAND-LINE: --finite-model-find ; EXPECT: unsat (benchmark Isabelle :status sat diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt index 4fe592638..97a585090 100644 --- a/test/regress/regress0/fmf/QEpres-uf.855035.smt +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --mbqi=gen-ev +; COMMAND-LINE: --finite-model-find ; EXPECT: sat (benchmark Isabelle :status sat diff --git a/test/regress/regress1/fmf/nlp042+1.smt2 b/test/regress/regress1/fmf/nlp042+1.smt2 index 567a3c0b7..6159f0b41 100644 --- a/test/regress/regress1/fmf/nlp042+1.smt2 +++ b/test/regress/regress1/fmf/nlp042+1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --mbqi=abs --no-check-models +; COMMAND-LINE: --finite-model-find --no-check-models ; EXPECT: sat (set-logic UF) (set-info :status sat) |