From a97944b850f201fd692aa870e830b8fa0369c541 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 9 Sep 2016 14:14:09 -0500 Subject: Support for separation logic + EPR. Refactor preprocessing of sep.nil, only allow sep disequal card constants when type is monotonic. Update logics on sep regressions. --- test/regress/regress0/sep/sep-neg-nstrict2.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress0/sep/sep-neg-nstrict2.smt2') diff --git a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 index e71e6a51a..7ada6ff06 100644 --- a/test/regress/regress0/sep/sep-neg-nstrict2.smt2 +++ b/test/regress/regress0/sep/sep-neg-nstrict2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) -- cgit v1.2.3