diff --git a/src/smtsolvers/CoreSMTSolver.cc b/src/smtsolvers/CoreSMTSolver.cc
index 847e2b7eb..12c85c445 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)] = 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.