diff options
Diffstat (limited to 'test/regress/regress0/sep/crash1220.smt2')
| -rwxr-xr-x | test/regress/regress0/sep/crash1220.smt2 | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress0/sep/crash1220.smt2 b/test/regress/regress0/sep/crash1220.smt2 new file mode 100755 index 000000000..a0fc5a187 --- /dev/null +++ b/test/regress/regress0/sep/crash1220.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-const x Int) +(declare-const a Int) + +(declare-const y Int) +(declare-const b Int) + +(assert (or (pto x a) (sep (pto x a) (pto y b)))) +(assert (or (not (pto x a)) (sep (not (pto x a)) (not (pto y b))))) + +(check-sat) |