From 481819ff29acf208b2e6f8243288763d4fa42c4d Mon Sep 17 00:00:00 2001
From: "Ola Wingbrant (sssowo)" <ola.wingbrant@scania.com>
Date: Mon, 10 Jun 2024 14:23:24 +0200
Subject: [PATCH] Add changes from theory-of-heaps-translation-thesis-version

---
 src/tricera/Main.scala                      |  2 +-
 src/tricera/concurrency/CCReader.scala      |  2 +-
 src/tricera/postprocessor/ADTExploder.scala | 27 ++++++++++++++++++---
 3 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala
index 554eab9..2ccd6fb 100644
--- a/src/tricera/Main.scala
+++ b/src/tricera/Main.scala
@@ -678,7 +678,7 @@ class Main (args: Array[String]) {
                     printlnDebug(postClauses.toString)
 
                     acslProcessedSolution = addClauses(
-                      postClauses,ctx.prePred.pred, acslProcessedSolution)
+                      postClauses,ctx.postPred.pred, acslProcessedSolution)
                   }
 
                   val printHeapExprProcessors = Seq(
diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala
index 6e4fce8..0999153 100644
--- a/src/tricera/concurrency/CCReader.scala
+++ b/src/tricera/concurrency/CCReader.scala
@@ -696,7 +696,7 @@ class CCReader private (prog              : Program,
 
   if (modelHeap) {
     GlobalVars addVar heapVar
-    GlobalVars.inits += CCTerm(heap.emptyHeap(), CCHeap(heap), None)
+    GlobalVars.inits += CCTerm(heapTerm, CCHeap(heap), None)
     variableHints += List()
   }
 
diff --git a/src/tricera/postprocessor/ADTExploder.scala b/src/tricera/postprocessor/ADTExploder.scala
index 0753622..6bc4fa6 100644
--- a/src/tricera/postprocessor/ADTExploder.scala
+++ b/src/tricera/postprocessor/ADTExploder.scala
@@ -64,6 +64,23 @@ object ADTExploder extends SolutionProcessor
                            subres: Seq[IExpression]) : IExpression = {
 
       import IExpression._
+      def checkExplodable(originalEq : IEquation, ctorFun : IFunction,
+                       lhsIsCtor : Boolean) : Boolean = {
+        val newEq = originalEq update subres
+        val (newFunApp, selectorTerms, newRootTerm) =
+          if (lhsIsCtor) {
+            val Eq(newFunApp@IFunApp(_, selectorTerms), newRootTerm) = newEq
+            (newFunApp, selectorTerms, newRootTerm)
+          } else {
+            val Eq(newRootTerm, newFunApp@IFunApp(_, selectorTerms)) = newEq
+            (newFunApp, selectorTerms, newRootTerm)
+          }
+        val adtTerm = getADTTerm(newFunApp).get
+        val adt = adtTerm.adtSort.adtTheory
+        val ctorIndex = adt.constructors.indexOf(ctorFun)
+        ctorIndex != -1
+      }
+
       def explodeADTSelectors (originalEq : IEquation, ctorFun : IFunction,
                                lhsIsCtor : Boolean) = {
         val newEq = originalEq update subres
@@ -85,10 +102,12 @@ object ADTExploder extends SolutionProcessor
       }
 
       t match {
-        case e@Eq(funApp@IFunApp(fun, _), _) if getADTTerm(funApp).nonEmpty =>
-          explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = true)
-        case e@Eq(_, funApp@IFunApp(fun, _)) if getADTTerm(funApp).nonEmpty =>
-          explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = false)
+        case e@Eq(funApp@IFunApp(fun, _), _) if getADTTerm(funApp).nonEmpty &&
+              checkExplodable(e.asInstanceOf[IEquation], fun, lhsIsCtor = true) =>
+                explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = true)
+        case e@Eq(_, funApp@IFunApp(fun, _)) if getADTTerm(funApp).nonEmpty &&
+              checkExplodable(e.asInstanceOf[IEquation], fun, lhsIsCtor = false) =>
+                explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = false)
         case t@IFunApp(f,_) =>
           val newApp = t update subres
           (for (theory <- TheoryRegistry lookupSymbol f;