From 879f57ac2ed6e8bc4dd8de64177857a03b1b6e1d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= <antti.hyvarinen@gmail.com>
Date: Mon, 4 Apr 2022 22:32:15 +0200
Subject: [PATCH 1/2] CoreSMTSolver: sticky polarities

---
 src/smtsolvers/CoreSMTSolver.cc | 10 +++++++++-
 src/smtsolvers/CoreSMTSolver.h  |  2 ++
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc
index 847e2b7eb..40433814a 100644
--- a/src/smtsolvers/CoreSMTSolver.cc
+++ b/src/smtsolvers/CoreSMTSolver.cc
@@ -236,6 +236,7 @@ Var CoreSMTSolver::newVar(bool sign, bool dvar)
     trail    .capacity(v+1);
     setDecisionVar(v, dvar);
     polarity    .push((char)sign);
+    saved_polar.push(true);
 
 #if CACHE_POLARITY
     prev_polarity.push(toInt(l_Undef));
@@ -406,6 +407,12 @@ void CoreSMTSolver::cancelUntil(int level)
 {
     if (decisionLevel() > level)
     {
+        if (trail.size() > longest_trail) {
+            for (auto p : trail) {
+                saved_polar[var(p)] = not sign(p);
+            }
+            longest_trail = trail.size();
+        }
         for (int c = trail.size()-1; c >= trail_lim[level]; c--)
         {
             Var      x  = var(trail[c]);
@@ -570,7 +577,8 @@ Lit CoreSMTSolver::choosePolarity(Var next) {
     }
     switch ( polarity_mode ) {
         case polarity_true:
-            sign = false;
+//            sign = false;
+            sign = saved_polar[next];
             break;
         case polarity_false:
             sign = true;
diff --git a/src/smtsolvers/CoreSMTSolver.h b/src/smtsolvers/CoreSMTSolver.h
index 7bbf691b4..b092b5f0d 100644
--- a/src/smtsolvers/CoreSMTSolver.h
+++ b/src/smtsolvers/CoreSMTSolver.h
@@ -319,6 +319,8 @@ class CoreSMTSolver
     double              var_inc;          // Amount to bump next variable with.
     OccLists<Lit, vec<Watcher>, WatcherDeleted>  watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
     vec<lbool>          assigns;          // The current assignments (lbool:s stored as char:s).
+    vec<bool>           saved_polar;
+    int                 longest_trail = 0;
     vec<bool>           var_seen;
     vec<char>           polarity;         // The preferred polarity of each variable.
     vec<char>           decision;         // Declares if a variable is eligible for selection in the decision heuristic.

From fa2481fea2d0225bc9d0030527a781593d88c223 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= <antti.hyvarinen@gmail.com>
Date: Tue, 5 Apr 2022 10:04:33 +0200
Subject: [PATCH 2/2] CoreSMTSolver: Sticky polarities without inverse

---
 src/smtsolvers/CoreSMTSolver.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc
index 40433814a..12c85c445 100644
--- a/src/smtsolvers/CoreSMTSolver.cc
+++ b/src/smtsolvers/CoreSMTSolver.cc
@@ -409,7 +409,7 @@ void CoreSMTSolver::cancelUntil(int level)
     {
         if (trail.size() > longest_trail) {
             for (auto p : trail) {
-                saved_polar[var(p)] = not sign(p);
+                saved_polar[var(p)] = sign(p);
             }
             longest_trail = trail.size();
         }