diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2021-07-26 20:49:16 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2021-07-26 20:49:16 -0500 |
| commit | 5ffe05a0b2769ba0b4b338b19e21c818bc1047a7 (patch) | |
| tree | f4d835bafd1d2997668feda4cfd738b7f5672054 /test | |
| parent | 48254fd071805e1594fa4435e557391cf6795a05 (diff) | |
Miscellaneous sync to master
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/bv/bv_to_int_bvmul2.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/sort-infer-typed-082718.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress0/proofs/scope.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress2/instance_1444.smtv1.smt2 | 1 |
4 files changed, 5 insertions, 5 deletions
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 index ebec5169a..91e0c45fd 100644 --- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 @@ -2,9 +2,9 @@ ; EXPECT: unsat (set-logic QF_BV) (declare-fun T4_180 () (_ BitVec 32)) -(assert (and -(= (bvmul T4_180 (_ bv1056 32)) (_ bv0 32)) -(not (= (bvmul T4_180 (_ bv1408 32)) (_ bv0 32))) +(assert (and +(= (bvmul T4_180 (_ bv1056 32)) (_ bv0 32)) +(not (= (bvmul T4_180 (_ bv1408 32)) (_ bv0 32))) ) ) (check-sat) diff --git a/test/regress/regress0/fmf/sort-infer-typed-082718.smt2 b/test/regress/regress0/fmf/sort-infer-typed-082718.smt2 index 3e837cc73..9ee1fa5eb 100644 --- a/test/regress/regress0/fmf/sort-infer-typed-082718.smt2 +++ b/test/regress/regress0/fmf/sort-infer-typed-082718.smt2 @@ -3,3 +3,4 @@ (set-logic ALL) (assert (not (exists ((X Int)) (not (= X 12)) ))) (check-sat) + diff --git a/test/regress/regress0/proofs/scope.smt2 b/test/regress/regress0/proofs/scope.smt2 index 133dd0c34..7a324952e 100644 --- a/test/regress/regress0/proofs/scope.smt2 +++ b/test/regress/regress0/proofs/scope.smt2 @@ -51,4 +51,4 @@ (assert (! (= (f2$ x2$ x4$) (f2$ (f5a$ x9$ x10$) x3$)) :named a7)) (assert (! (not false) :named a8)) (check-sat) -(get-proof) +(get-proof)
\ No newline at end of file diff --git a/test/regress/regress2/instance_1444.smtv1.smt2 b/test/regress/regress2/instance_1444.smtv1.smt2 index b752b7838..47d3fda52 100644 --- a/test/regress/regress2/instance_1444.smtv1.smt2 +++ b/test/regress/regress2/instance_1444.smtv1.smt2 @@ -1,5 +1,4 @@ ; COMMAND-LINE: --no-produce-proofs -; EXPECT: unsat (set-option :incremental false) (set-info :status unsat) (set-logic QF_UF) |