diff options
Diffstat (limited to 'test/regress/regress0/fmf')
-rw-r--r-- | test/regress/regress0/fmf/ALG008-1.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/Hoare-z3.931718.smt | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/PUZ001+1.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/QEpres-uf.855035.smt | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/agree466.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/agree467.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/array_card.smt2 | 1 | ||||
-rwxr-xr-x | test/regress/regress0/fmf/bug0909.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/german169.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/german73.smt2 | 1 | ||||
-rw-r--r-- | test/regress/regress0/fmf/refcount24.cvc.smt2 | 1 |
12 files changed, 0 insertions, 12 deletions
diff --git a/test/regress/regress0/fmf/ALG008-1.smt2 b/test/regress/regress0/fmf/ALG008-1.smt2 index 018006f45..2c3bab80d 100644 --- a/test/regress/regress0/fmf/ALG008-1.smt2 +++ b/test/regress/regress0/fmf/ALG008-1.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -; EXIT: 10 ;%-------------------------------------------------------------------------- ;% File : ALG008-1 : TPTP v5.4.0. Released v2.2.0. ;% Domain : General Algebra diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt index 644d29737..536bc241f 100644 --- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt +++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt @@ -1,6 +1,5 @@ % COMMAND-LINE: --finite-model-find % EXPECT: unsat -% EXIT: 20 (benchmark Isabelle :status sat :logic AUFLIA diff --git a/test/regress/regress0/fmf/Hoare-z3.931718.smt b/test/regress/regress0/fmf/Hoare-z3.931718.smt index 0b6fd0349..754e19e88 100644 --- a/test/regress/regress0/fmf/Hoare-z3.931718.smt +++ b/test/regress/regress0/fmf/Hoare-z3.931718.smt @@ -1,6 +1,5 @@ % COMMAND-LINE: --finite-model-find % EXPECT: sat -% EXIT: 10 (benchmark Isabelle :status sat :logic AUFLIA diff --git a/test/regress/regress0/fmf/PUZ001+1.smt2 b/test/regress/regress0/fmf/PUZ001+1.smt2 index 4bcbf51c6..bf156367e 100644 --- a/test/regress/regress0/fmf/PUZ001+1.smt2 +++ b/test/regress/regress0/fmf/PUZ001+1.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: unsat -; EXIT: 20 ;%------------------------------------------------------------------------------ ;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0. ;% Domain : Puzzles diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt index 95ab0cb34..980e5fd49 100644 --- a/test/regress/regress0/fmf/QEpres-uf.855035.smt +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt @@ -1,6 +1,5 @@ % COMMAND-LINE: --finite-model-find % EXPECT: sat -% EXIT: 10 (benchmark Isabelle :status sat :logic AUFLIA diff --git a/test/regress/regress0/fmf/agree466.smt2 b/test/regress/regress0/fmf/agree466.smt2 index 2a021ea9b..bfe48195b 100644 --- a/test/regress/regress0/fmf/agree466.smt2 +++ b/test/regress/regress0/fmf/agree466.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -; EXIT: 10 ; Preamble -------------- (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress0/fmf/agree467.smt2 b/test/regress/regress0/fmf/agree467.smt2 index 09e16dfe3..1bfdb9f83 100644 --- a/test/regress/regress0/fmf/agree467.smt2 +++ b/test/regress/regress0/fmf/agree467.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: unsat -; EXIT: 20 ; Preamble -------------- (set-logic ALL_SUPPORTED) (set-info :status unsat) diff --git a/test/regress/regress0/fmf/array_card.smt2 b/test/regress/regress0/fmf/array_card.smt2 index 9ee00d13a..42293e224 100644 --- a/test/regress/regress0/fmf/array_card.smt2 +++ b/test/regress/regress0/fmf/array_card.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -; EXIT: 10 (set-logic AUFLIA) (set-option :produce-models true) (declare-sort U 0) diff --git a/test/regress/regress0/fmf/bug0909.smt2 b/test/regress/regress0/fmf/bug0909.smt2 index 39862b8d6..9577e8f57 100755 --- a/test/regress/regress0/fmf/bug0909.smt2 +++ b/test/regress/regress0/fmf/bug0909.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: unsat -; EXIT: 20 ; Preamble -------------- (set-option :produce-models true) (set-logic ALL_SUPPORTED) diff --git a/test/regress/regress0/fmf/german169.smt2 b/test/regress/regress0/fmf/german169.smt2 index f0906d6b5..3558715a8 100644 --- a/test/regress/regress0/fmf/german169.smt2 +++ b/test/regress/regress0/fmf/german169.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -; EXIT: 10 (set-logic ALL_SUPPORTED) (set-info :status sat) (declare-datatypes () ((UNIT (Unit)))) diff --git a/test/regress/regress0/fmf/german73.smt2 b/test/regress/regress0/fmf/german73.smt2 index 388a53624..e1d499972 100644 --- a/test/regress/regress0/fmf/german73.smt2 +++ b/test/regress/regress0/fmf/german73.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: unsat -; EXIT: 20 (set-logic ALL_SUPPORTED) (set-info :status unsat) (declare-datatypes () ((UNIT (Unit)))) diff --git a/test/regress/regress0/fmf/refcount24.cvc.smt2 b/test/regress/regress0/fmf/refcount24.cvc.smt2 index bf042c9b2..e3b6957d0 100644 --- a/test/regress/regress0/fmf/refcount24.cvc.smt2 +++ b/test/regress/regress0/fmf/refcount24.cvc.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -; EXIT: 10 (set-logic ALL_SUPPORTED) (set-info :smt-lib-version 2.0) (set-info :category "unknown") |