From: Andres Notzli <andres.noetzli@gmail.com>
Date: Mon, 12 Dec 2016 09:55:36 +0000 (-0800)
Subject: Fix split-find-unsat-w-emp test
X-Git-Tag: cvc5-1.0.0~5940^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e6bb2eb7299f60a334a633a33e9085e1bc936a85;p=cvc5.git

Fix split-find-unsat-w-emp test

Commit 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the
split-find-unsat-w-emp test, this commit fixes that.
---

diff --git a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
index 10e509e05..c606d0ab6 100644
--- a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
+++ b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2
@@ -10,7 +10,7 @@
 (declare-const c Int)
 
 (assert (and
-        (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (emp x)) ))
+        (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (emp x x)) ))
         (sep (pto x a) (pto y b))
   )
 )