diff options
Diffstat (limited to 'test/regress/regress1/sep/sep-find2.smt2')
| -rw-r--r-- | test/regress/regress1/sep/sep-find2.smt2 | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress1/sep/sep-find2.smt2 b/test/regress/regress1/sep/sep-find2.smt2 new file mode 100644 index 000000000..356f866c1 --- /dev/null +++ b/test/regress/regress1/sep/sep-find2.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) + +(declare-const x1 Int) +(declare-const x2 Int) +(declare-const x3 Int) +(declare-const x4 Int) +(declare-const x5 Int) +(declare-const x6 Int) +(declare-const x7 Int) + +(declare-const a1 Int) +(declare-const a2 Int) + +(assert (and +(sep (pto x1 a1) (pto x2 a2) (pto x4 a2) (pto x5 a2) (pto x6 a2) (pto x7 a2)) +(sep (pto x1 a1) (pto x3 a2)) +)) + +(assert (distinct x3 x2 x4 x5 x6 x7)) + +(check-sat) |