diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index f87261dcf..9c77dec17 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -93,7 +93,8 @@ class fm_tactic : public tactic {
                     expr * lhs = to_app(l)->get_arg(0);
                     expr * rhs = to_app(l)->get_arg(1);
                     rational c;
-                    u.is_numeral(rhs, c);
+                    if (!u.is_numeral(rhs, c))
+                        return NONE;
                     if (neg)
                         c.neg();
                     unsigned num_mons;
@@ -112,7 +113,8 @@ class fm_tactic : public tactic {
                         expr * xi;
                         rational ai_val;
                         if (u.is_mul(monomial, ai, xi)) {
-                            u.is_numeral(ai, ai_val);
+                            if (!u.is_numeral(ai, ai_val))
+                                return NONE;
                         }
                         else {
                             xi     = monomial;
@@ -120,7 +122,8 @@ class fm_tactic : public tactic {
                         }
                         if (u.is_to_real(xi))
                             xi = to_app(xi)->get_arg(0);
-                        SASSERT(is_uninterp_const(xi));
+                        if (!is_uninterp_const(xi))
+                            return NONE;
                         if (x == to_app(xi)->get_decl()) {
                             a_val = ai_val;
                             if (neg)
@@ -129,7 +132,8 @@ class fm_tactic : public tactic {
                         else {
                             expr_ref val(m);
                             val = ev(monomial);
-                            SASSERT(u.is_numeral(val));
+                            if (!u.is_numeral(val))
+                                return NONE;
                             rational tmp;
                             u.is_numeral(val, tmp);
                             if (neg)
diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp
index 5b889efe6..95638cef7 100644
--- a/src/tactic/core/pb_preprocess_tactic.cpp
+++ b/src/tactic/core/pb_preprocess_tactic.cpp
@@ -44,6 +44,7 @@ class pb_preprocess_tactic : public tactic {
     struct rec { unsigned_vector pos, neg; rec() { } };
     typedef obj_map<app, rec> var_map;
     ast_manager&     m;
+    expr_ref_vector  m_trail;
     pb_util          pb;
     var_map          m_vars;    
     unsigned_vector  m_ge;
@@ -99,7 +100,7 @@ class pb_preprocess_tactic : public tactic {
 
 public:
     pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): 
-        m(m), pb(m), m_r(m) {}
+        m(m), m_trail(m), pb(m), m_r(m) {}
 
     ~pb_preprocess_tactic() override {}
 
@@ -121,6 +122,7 @@ public:
         g->inc_depth();        
         result.push_back(g.get());       
         while (simplify(g, *pp));
+        m_trail.reset();
         // decompose(g);
     }
 
@@ -406,6 +408,7 @@ private:
     void insert(unsigned i, app* e, bool pos) {
         SASSERT(is_uninterp_const(e));
         if (!m_vars.contains(e)) {
+            m_trail.push_back(e);
             m_vars.insert(e, rec());
         }
         if (pos) {