diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 739a9e61a..f68457383 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -6449,7 +6449,7 @@ class Tactic:
 
 def _to_goal(a):
     if isinstance(a, BoolRef):
-        goal = Goal()
+        goal = Goal(a.ctx)
         goal.add(a)
         return goal
     else:
diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index 6fd156e41..2717e4a92 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -820,6 +820,7 @@ public:
         }
     }
 
+private:
     // Update the assignment of variable v, that is,
     // m_assignment[v] += inc
     // This method also stores the old value of v in the assignment stack.
@@ -829,6 +830,12 @@ public:
         m_assignment[v] += inc;
     }
 
+public:
+
+    void inc_assignment(dl_var v, numeral const& inc) {
+        m_assignment[v] += inc;
+    }    
+
 
     struct every_var_proc {
         bool operator()(dl_var v) const {
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 8463eb17f..6039b208a 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -752,7 +752,8 @@ namespace smt {
 
             for (unsigned j = 0; j < zero_v.size(); ++j) {
                 int v = zero_v[j];
-                m_graph.acc_assignment(v, numeral(-1));
+                
+                m_graph.inc_assignment(v, numeral(-1));
                 th_var k = from_var(v);
                 if (!is_parity_ok(k)) {
                     todo.push_back(k);