diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index ec5d953bf..9648fdb0e 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -436,6 +436,7 @@ namespace smt {
     theory_pb::theory_pb(context& ctx):
         theory(ctx, ctx.get_manager().mk_family_id("pb")),
         m_params(ctx.get_fparams()),
+        m_mpz_trail(m_mpz_mgr),
         pb(ctx.get_manager()),
         m_restart_lim(3),
         m_restart_inc(0),
@@ -1106,8 +1107,10 @@ namespace smt {
        and/or relatively few compared to number of argumets.
      */
     void theory_pb::assign_ineq(ineq& c, bool is_true) {
-        ctx.push_trail(value_trail<context, scoped_mpz>(c.m_max_sum));
-        ctx.push_trail(value_trail<context, scoped_mpz>(c.m_min_sum));
+        m_mpz_trail.push_back(c.m_max_sum);
+        m_mpz_trail.push_back(c.m_min_sum);
+        ctx.push_trail(scoped_value_trail<context, scoped_mpz, scoped_mpz_vector>(c.m_max_sum, m_mpz_trail));
+        ctx.push_trail(scoped_value_trail<context, scoped_mpz, scoped_mpz_vector>(c.m_min_sum, m_mpz_trail));
         ctx.push_trail(value_trail<context, unsigned>(c.m_nfixed));
 
         SASSERT(c.is_ge());
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 150b72744..2d62bb7ac 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -271,6 +271,7 @@ namespace smt {
 
         svector<var_info>        m_var_infos; 
         mutable unsynch_mpz_manager      m_mpz_mgr;        // Simplex: manager mpz numerals
+        scoped_mpz_vector        m_mpz_trail;
         unsigned_vector          m_ineqs_trail;
         unsigned_vector          m_ineqs_lim;
         literal_vector           m_literals;    // temporary vector
diff --git a/src/util/trail.h b/src/util/trail.h
index b822b2456..031ccdef2 100644
--- a/src/util/trail.h
+++ b/src/util/trail.h
@@ -56,6 +56,29 @@ public:
     }
 };
 
+
+    
+template<typename Ctx, typename T, typename Ts>
+class scoped_value_trail : public trail<Ctx> {
+    T & m_value;
+    Ts & m_values;
+    
+public:
+    scoped_value_trail(T & value, Ts& values):
+        m_value(value),
+        m_values(values) {
+    }
+    
+    ~scoped_value_trail() override {
+    }
+    
+    void undo(Ctx & ctx) override {
+        m_value = m_values.back();
+        m_values.pop_back();
+    }
+};
+
+
 template<typename Ctx>
 class reset_flag_trail : public trail<Ctx> {
     bool & m_value;