diff options
Diffstat (limited to 'test')
-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) |