diff options
Diffstat (limited to 'test/regress/regress1/nl/issue5660-mb-success.smt2')
| -rw-r--r-- | test/regress/regress1/nl/issue5660-mb-success.smt2 | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/regress1/nl/issue5660-mb-success.smt2 b/test/regress/regress1/nl/issue5660-mb-success.smt2 new file mode 100644 index 000000000..6284b0580 --- /dev/null +++ b/test/regress/regress1/nl/issue5660-mb-success.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_AUFNRA) +(set-info :status sat) +(declare-fun r2 () Real) +(declare-fun r9 () Real) +(declare-fun r13 () Real) +(declare-fun ufrb5 (Real Real Real Real Real) Bool) +(declare-fun v3 () Bool) +(declare-fun v4 () Bool) +(declare-fun arr0 () (Array Bool Real)) +(declare-fun arr1 () (Array Bool (Array Bool Real))) +(declare-fun v5 () Bool) +(declare-fun v7 () Bool) +(declare-fun v8 () Bool) +(declare-fun v71 () Bool) +(declare-fun v81 () Bool) +(declare-fun v161 () Bool) +(assert (or v161 (and v3 (not v7)))) +(assert (or v8 (distinct v7 (and v7 v81) (ufrb5 0.0 1.0 0.0 1.0 (/ r13 r9))))) +(assert (or v161 (distinct v71 v8 (= v4 v81)))) +(assert (or v81 (= arr0 (store (select (store arr1 (xor v81 (and (= r2 1.0) (= r13 1))) arr0) v7) v81 (select (store arr0 v5 1.0) false))))) +(check-sat) |