From c9edfeabd6a1f7933d04a88d94e7ac4208fbcfc8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 2 Jun 2022 11:37:53 -0500
Subject: [PATCH] Fix missing conclusion for sep pto neg prop (#8844)

Was introduced in the refactoring in #8768.

Fixes #8841.
---
 src/theory/sep/theory_sep.cpp                 | 27 +++++++++++++------
 test/regress/cli/CMakeLists.txt               |  1 +
 .../cli/regress0/sep/issue8841-neg-prop.smt2  | 13 +++++++++
 3 files changed, 33 insertions(+), 8 deletions(-)
 create mode 100644 test/regress/cli/regress0/sep/issue8841-neg-prop.smt2

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 048d93e80..75484ceb0 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1825,7 +1825,23 @@ bool TheorySep::checkPto(HeapAssertInfo* e, Node p, bool polarity)
       else if (polarity != pol)
       {
         // a positive and negative pto
-        if (!areDisequal(pval, qval))
+        bool isSat = false;
+        std::vector<Node> conc;
+        // based on the lemma below, either the domain or range has to be
+        // disequal. We iterate on each child of the pto
+        for (size_t j = 0; j < 2; j++)
+        {
+          if (areDisequal(p[0][j], q[0][j]))
+          {
+            isSat = true;
+            break;
+          }
+          if (p[0][j] != q[0][j])
+          {
+            conc.push_back(p[0][j].eqNode(q[0][j]).notNode());
+          }
+        }
+        if (!isSat)
         {
           std::vector<Node> exp;
           if (plbl != qlbl)
@@ -1839,16 +1855,11 @@ bool TheorySep::checkPto(HeapAssertInfo* e, Node p, bool polarity)
           Node neg = polarity ? q : p;
           exp.push_back(pos);
           exp.push_back(neg.notNode());
-          std::vector<Node> conc;
-          if (pval != qval)
-          {
-            conc.push_back(pval.eqNode(qval).notNode());
-          }
           Node concn = nm->mkOr(conc);
           Trace("sep-pto") << "prop neg/pos: " << concn << " by " << exp
                            << std::endl;
-          // (label (pto x y) A) ^ ~(label (pto z w) B) ^ A = B => y != w
-          // or (label (pto x y) A) ^ ~(label (pto z y) B) ^ A = B => false
+          // (label (pto x y) A) ^ ~(label (pto z w) B) ^ A = B =>
+          // (x != z or y != w)
           sendLemma(exp, concn, InferenceId::SEP_PTO_NEG_PROP);
         }
       }
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 4ef2a64c7..12f8fd4c8 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1205,6 +1205,7 @@ set(regress_0_tests
   regress0/sep/issue3720-check-model.smt2
   regress0/sep/issue5343-err.smt2
   regress0/sep/issue8659-wand-diff-heaps.smt2
+  regress0/sep/issue8841-neg-prop.smt2
   regress0/sep/nemp.smt2
   regress0/sep/nil-no-elim.smt2
   regress0/sep/nspatial-simp.smt2
diff --git a/test/regress/cli/regress0/sep/issue8841-neg-prop.smt2 b/test/regress/cli/regress0/sep/issue8841-neg-prop.smt2
new file mode 100644
index 000000000..15b1edd32
--- /dev/null
+++ b/test/regress/cli/regress0/sep/issue8841-neg-prop.smt2
@@ -0,0 +1,13 @@
+; DISABLE-TESTER: model
+(set-logic QF_ALL)
+(set-info :status sat)
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x1 Loc)
+(declare-const x2 Loc)
+
+(assert (pto x1 x2))
+(assert (not (pto x2 x2)))
+
+(check-sat)
-- 
2.30.2