diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 33d09bc8e..5e67d65fa 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -744,7 +744,6 @@ basic_decl_plugin::basic_decl_plugin():
     m_th_assumption_add_decl(nullptr),
     m_th_lemma_add_decl(nullptr),
     m_redundant_del_decl(nullptr),
-    m_clause_trail_decl(nullptr),
     m_hyper_res_decl0(nullptr) {
 }
 
@@ -835,9 +834,9 @@ func_decl * basic_decl_plugin::mk_compressed_proof_decl(char const * name, basic
 
 func_decl * basic_decl_plugin::mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, ptr_vector<func_decl> & cache) {
     if (num_parents >= cache.size()) {
-        cache.resize(num_parents+1);
+        cache.resize(num_parents+1, nullptr);
     }
-    if (cache[num_parents] == 0) {
+    if (!cache[num_parents]) {
         cache[num_parents] = mk_proof_decl(name, k, num_parents);
     }
     return cache[num_parents];
@@ -920,7 +919,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
     case PR_TH_ASSUMPTION_ADD:            return mk_proof_decl("add-th-assume", k, num_parents, m_th_assumption_add_decl);
     case PR_TH_LEMMA_ADD:                 return mk_proof_decl("add-th-lemma", k, num_parents, m_th_lemma_add_decl);
     case PR_REDUNDANT_DEL:                return mk_proof_decl("del-redundant", k, num_parents, m_redundant_del_decl);
-    case PR_CLAUSE_TRAIL:                 return mk_proof_decl("proof-trail", k, num_parents, m_clause_trail_decl);
+    case PR_CLAUSE_TRAIL:                 return mk_proof_decl("proof-trail", k, num_parents);
     default:
         UNREACHABLE();
         return nullptr;
@@ -1041,7 +1040,6 @@ void basic_decl_plugin::finalize() {
     DEC_REF(m_th_assumption_add_decl);
     DEC_REF(m_th_lemma_add_decl);
     DEC_REF(m_redundant_del_decl);
-    DEC_REF(m_clause_trail_decl);
     DEC_ARRAY_REF(m_apply_def_decls);
     DEC_ARRAY_REF(m_nnf_pos_decls);
     DEC_ARRAY_REF(m_nnf_neg_decls);
@@ -1900,6 +1898,22 @@ ast * ast_manager::register_node_core(ast * n) {
     default:
         break;
     }
+
+#if 0
+    // std::cout << n->m_id << " " << n->hash() << "\n";
+    if (n->m_id == 1523) {
+        std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
+    }
+    if (n->m_id == 1524) {
+        std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
+        VERIFY(false);
+    }
+    if (n->m_id == 1525) {
+        std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
+    }
+    //VERIFY(n->m_id != 1549);
+    //VERIFY(s_count != 2);
+#endif
     return n;
 }
 
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 4bd5b4bae..9f61911a5 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1167,7 +1167,6 @@ protected:
     func_decl * m_th_assumption_add_decl;
     func_decl * m_th_lemma_add_decl;
     func_decl * m_redundant_del_decl;
-    func_decl * m_clause_trail_decl;
     ptr_vector<func_decl> m_apply_def_decls;
     ptr_vector<func_decl> m_nnf_pos_decls;
     ptr_vector<func_decl> m_nnf_neg_decls;
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index 3a5fba27c..c8403e2b1 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -126,7 +126,7 @@ namespace algebraic_numbers {
 
         bool acell_inv(algebraic_cell const& c) {
             auto s = upm().eval_sign_at(c.m_p_sz, c.m_p, lower(&c));
-            return s == polynomial::sign_zero || c.m_sign_lower == (s == polynomial::sign_neg);
+            return s == sign_zero || c.m_sign_lower == (s == sign_neg);
         }
 
         void checkpoint() {
@@ -262,7 +262,7 @@ namespace algebraic_numbers {
 
             SASSERT(bqm().ge(upper(c), candidate));
 
-            if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == polynomial::sign_zero) {
+            if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == sign_zero) {
                 m_wrapper.set(a, candidate);
                 return true;
             }
@@ -325,7 +325,7 @@ namespace algebraic_numbers {
             SASSERT(bqm().ge(upper(c), candidate));
 
             // Find if candidate is an actual root
-            if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == polynomial::sign_zero) {
+            if (bqm().lt(lower(c), candidate) && upm().eval_sign_at(c->m_p_sz, c->m_p, candidate) == sign_zero) {
                 saved_a.restore_if_too_small();
                 set(a, candidate);
                 return true;
@@ -371,8 +371,8 @@ namespace algebraic_numbers {
             return c;
         }
 
-        polynomial::sign sign_lower(algebraic_cell * c) const {
-            return c->m_sign_lower == 0 ? polynomial::sign_pos : polynomial::sign_neg;
+        sign sign_lower(algebraic_cell * c) const {
+            return c->m_sign_lower == 0 ? sign_pos : sign_neg;
         }
 
         mpbq const & lower(algebraic_cell const * c) const { return c->m_interval.lower(); }
@@ -384,11 +384,11 @@ namespace algebraic_numbers {
         mpbq & upper(algebraic_cell * c) { return c->m_interval.upper(); }
 
         void update_sign_lower(algebraic_cell * c) {
-            polynomial::sign sl = upm().eval_sign_at(c->m_p_sz, c->m_p, lower(c));
+            sign sl = upm().eval_sign_at(c->m_p_sz, c->m_p, lower(c));
             // The isolating intervals are refinable. Thus, the polynomial has opposite signs at lower and upper.
-            SASSERT(sl != polynomial::sign_zero);
+            SASSERT(sl != sign_zero);
             SASSERT(upm().eval_sign_at(c->m_p_sz, c->m_p, upper(c)) == -sl);
-            c->m_sign_lower = sl == polynomial::sign_neg;
+            c->m_sign_lower = sl == sign_neg;
             SASSERT(acell_inv(*c));
         }
 
@@ -1607,14 +1607,14 @@ namespace algebraic_numbers {
             if (!bqm().is_zero(_lower) && !bqm().is_zero(_upper))
                 return;
             auto sign_l = sign_lower(cell_a);
-            SASSERT(!polynomial::is_zero(sign_l));
+            SASSERT(!::is_zero(sign_l));
             auto sign_u = -sign_l;
 
 #define REFINE_LOOP(BOUND, TARGET_SIGN)                                 \
             while (true) {                                              \
                 bqm().div2(BOUND);                                      \
-                polynomial::sign new_sign = upm().eval_sign_at(cell_a->m_p_sz, cell_a->m_p, BOUND); \
-                if (new_sign == polynomial::sign_zero) {                \
+                sign new_sign = upm().eval_sign_at(cell_a->m_p_sz, cell_a->m_p, BOUND); \
+                if (new_sign == sign_zero) {                \
                     /* found actual root */                             \
                     scoped_mpq r(qm());                                 \
                     to_mpq(qm(), BOUND, r);                             \
@@ -1689,10 +1689,10 @@ namespace algebraic_numbers {
         }
 
         // Todo: move to MPQ
-        int compare(mpq const & a, mpq const & b) {
+        ::sign compare(mpq const & a, mpq const & b) {
             if (qm().eq(a, b))
-                return 0;
-            return qm().lt(a, b) ? -1 : 1;
+                return sign_zero;
+            return qm().lt(a, b) ? sign_neg : sign_pos;
         }
 
         /**
@@ -1710,18 +1710,18 @@ namespace algebraic_numbers {
              p(b) == 0 then c == b
              (p(b) < 0) == (p(l) < 0) then c > b else c < b
         */
-        int compare(algebraic_cell * c, mpq const & b) {
+        ::sign compare(algebraic_cell * c, mpq const & b) {
             mpbq const & l = lower(c);
             mpbq const & u = upper(c);
             if (bqm().le(u, b))
-                return -1;
+                return sign_neg;
             if (bqm().ge(l, b))
-                return 1;
+                return sign_pos;
             // b is in the isolating interval (l, u)
             auto sign_b = upm().eval_sign_at(c->m_p_sz, c->m_p, b);
-            if (sign_b == polynomial::sign_zero)
-                return 0;
-            return sign_b == sign_lower(c) ? 1 : -1;
+            if (sign_b == sign_zero)
+                return sign_zero;
+            return sign_b == sign_lower(c) ? sign_pos : sign_neg;
         }
 
         // Return true if the polynomials of cell_a and cell_b are the same.
@@ -1729,7 +1729,7 @@ namespace algebraic_numbers {
             return upm().eq(cell_a->m_p_sz, cell_a->m_p, cell_b->m_p_sz, cell_b->m_p);
         }
 
-        int compare_core(numeral & a, numeral & b) {
+        ::sign compare_core(numeral & a, numeral & b) {
             SASSERT(!a.is_basic() && !b.is_basic());
             algebraic_cell * cell_a = a.to_algebraic();
             algebraic_cell * cell_b = b.to_algebraic();
@@ -1741,11 +1741,11 @@ namespace algebraic_numbers {
             #define COMPARE_INTERVAL()                  \
             if (bqm().le(a_upper, b_lower)) {           \
                 m_compare_cheap++;                      \
-                return -1;                              \
+                return sign_neg;                        \
             }                                           \
             if (bqm().ge(a_lower, b_upper)) {           \
                 m_compare_cheap++;                      \
-                return 1;                               \
+                return sign_pos;                        \
             }
 
             COMPARE_INTERVAL();
@@ -1755,7 +1755,7 @@ namespace algebraic_numbers {
             // the same root.
             if (compare_p(cell_a, cell_b)) {
                 m_compare_poly_eq++;
-                return 0;
+                return sign_zero;
             }
 
             TRACE("algebraic", tout << "comparing\n";
@@ -1786,8 +1786,8 @@ namespace algebraic_numbers {
                 }
             }
 
-			if (!m_limit.inc())
-				return 0;
+            if (!m_limit.inc())
+                return sign_zero;
 
             // make sure that intervals of a and b have the same magnitude
             int a_m      = magnitude(a_lower, a_upper);
@@ -1843,11 +1843,11 @@ namespace algebraic_numbers {
            TRACE("algebraic", tout << "comparing using sturm\n"; display_interval(tout, a); tout << "\n"; display_interval(tout, b); tout << "\n";
                  tout << "V: " << V << ", sign_lower(a): " << sign_lower(cell_a) << ", sign_lower(b): " << sign_lower(cell_b) << "\n";);
            if (V == 0)
-               return 0;
+               return sign_zero;
            if ((V < 0) == (sign_lower(cell_b) < 0))
-               return -1;
+               return sign_neg;
            else
-               return 1;
+               return sign_pos;
 
            // Here is an unexplored option for comparing numbers.
            //
@@ -1883,7 +1883,7 @@ namespace algebraic_numbers {
            //          (l1 - u2, u1 - l2) contains only one root of r(x)
         }
 
-        int compare(numeral & a, numeral & b) {
+        ::sign compare(numeral & a, numeral & b) {
             TRACE("algebraic", tout << "comparing: "; display_interval(tout, a); tout << " "; display_interval(tout, b); tout << "\n";);
             if (a.is_basic()) {
                 if (b.is_basic())
@@ -2002,7 +2002,7 @@ namespace algebraic_numbers {
         };
 
         polynomial::var_vector m_eval_sign_vars;
-        polynomial::sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
+        sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
             polynomial::manager & ext_pm = p.m();
             TRACE("anum_eval_sign", tout << "evaluating sign of: " << p << "\n";);
             while (true) {
@@ -2013,7 +2013,7 @@ namespace algebraic_numbers {
                     scoped_mpq r(qm());
                     ext_pm.eval(p, x2v_basic, r);
                     TRACE("anum_eval_sign", tout << "all variables are assigned to rationals, value of p: " << r << "\n";);
-                    return polynomial::to_sign(qm().sign(r));
+                    return ::to_sign(qm().sign(r));
                 }
                 catch (const opt_var2basic::failed &) {
                     // continue
@@ -2027,13 +2027,13 @@ namespace algebraic_numbers {
 
                 if (ext_pm.is_zero(p_prime)) {
                     // polynomial vanished after substituting rational values.
-                    return polynomial::sign_zero;
+                    return sign_zero;
                 }
 
                 if (is_const(p_prime)) {
                     // polynomial became the constant polynomial after substitution.
                     SASSERT(size(p_prime) == 1);
-                    return polynomial::to_sign(ext_pm.m().sign(ext_pm.coeff(p_prime, 0)));
+                    return to_sign(ext_pm.m().sign(ext_pm.coeff(p_prime, 0)));
                 }
 
                 // Try to find sign using intervals
@@ -2049,7 +2049,7 @@ namespace algebraic_numbers {
                     ext_pm.eval(p_prime, x2v_interval, ri);
                     TRACE("anum_eval_sign", tout << "evaluating using intervals: " << ri << "\n";);
                     if (!bqim().contains_zero(ri)) {
-                        return bqim().is_pos(ri) ? polynomial::sign_pos : polynomial::sign_neg;
+                        return bqim().is_pos(ri) ? sign_pos : sign_neg;
                     }
                     // refine intervals if magnitude > m_min_magnitude
                     bool refined = false;
@@ -2090,7 +2090,7 @@ namespace algebraic_numbers {
                 // Remark: m_zero_accuracy == 0 means use precise computation.
                 if (m_zero_accuracy > 0) {
                     // assuming the value is 0, since the result is in (-1/2^k, 1/2^k), where m_zero_accuracy = k
-                    return polynomial::sign_zero;
+                    return sign_zero;
                 }
 #if 0
                 // Evaluating sign using algebraic arithmetic
@@ -2163,7 +2163,7 @@ namespace algebraic_numbers {
                 bqm().div2k(mL, k);
                 bqm().div2k(L, k);
                 if (bqm().lt(mL, ri.lower()) && bqm().lt(ri.upper(), L))
-                    return polynomial::sign_zero;
+                    return sign_zero;
                 // keep refining ri until ri is inside (-L, L) or
                 // ri does not contain zero.
 
@@ -2186,11 +2186,11 @@ namespace algebraic_numbers {
                     TRACE("anum_eval_sign", tout << "evaluating using intervals: " << ri << "\n";
                           tout << "zero lower bound is: " << L << "\n";);
                     if (!bqim().contains_zero(ri)) {
-                        return bqim().is_pos(ri) ? polynomial::sign_pos : polynomial::sign_neg;
+                        return bqim().is_pos(ri) ? sign_pos : sign_neg;
                     }
 
                     if (bqm().lt(mL, ri.lower()) && bqm().lt(ri.upper(), L))
-                        return polynomial::sign_zero;
+                        return sign_zero;
 
                     for (auto x : xs) {
                         SASSERT(x2v.contains(x));
@@ -2265,7 +2265,7 @@ namespace algebraic_numbers {
                 checkpoint();
                 ext_var2num ext_x2v(m_wrapper, x2v, x, roots[i]);
                 TRACE("isolate_roots", tout << "filter_roots i: " << i << ", ext_x2v: x" << x << " -> "; display_root(tout, roots[i]); tout << "\n";);
-                polynomial::sign sign = eval_sign_at(p, ext_x2v);
+                sign sign = eval_sign_at(p, ext_x2v);
                 TRACE("isolate_roots", tout << "filter_roots i: " << i << ", result sign: " << sign << "\n";);
                 if (sign != 0)
                     continue;
@@ -2468,7 +2468,7 @@ namespace algebraic_numbers {
             }
         }
 
-        polynomial::sign eval_at_mpbq(polynomial_ref const & p, polynomial::var2anum const & x2v, polynomial::var x, mpbq const & v) {
+        sign eval_at_mpbq(polynomial_ref const & p, polynomial::var2anum const & x2v, polynomial::var x, mpbq const & v) {
             scoped_mpq  qv(qm());
             to_mpq(qm(), v, qv);
             scoped_anum av(m_wrapper);
@@ -2583,13 +2583,13 @@ namespace algebraic_numbers {
 
 #define DEFAULT_PRECISION 2
 
-        void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<polynomial::sign> & signs) {
+        void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<sign> & signs) {
             isolate_roots(p, x2v, roots);
             unsigned num_roots = roots.size();
             if (num_roots == 0) {
                 anum zero;
                 ext2_var2num ext_x2v(m_wrapper, x2v, zero);
-                polynomial::sign s = eval_sign_at(p, ext_x2v);
+                sign s = eval_sign_at(p, ext_x2v);
                 signs.push_back(s);
             }
             else {
@@ -2617,7 +2617,7 @@ namespace algebraic_numbers {
                 {
                     ext2_var2num ext_x2v(m_wrapper, x2v, w);
                     auto s = eval_sign_at(p, ext_x2v);
-                    SASSERT(s != polynomial::sign_zero);
+                    SASSERT(s != sign_zero);
                     signs.push_back(s);
                 }
 
@@ -2627,7 +2627,7 @@ namespace algebraic_numbers {
                     select(prev, curr, w);
                     ext2_var2num ext_x2v(m_wrapper, x2v, w);
                     auto s = eval_sign_at(p, ext_x2v);
-                    SASSERT(s != polynomial::sign_zero);
+                    SASSERT(s != sign_zero);
                     signs.push_back(s);
                 }
 
@@ -2635,7 +2635,7 @@ namespace algebraic_numbers {
                 {
                     ext2_var2num ext_x2v(m_wrapper, x2v, w);
                     auto s = eval_sign_at(p, ext_x2v);
-                    SASSERT(s != polynomial::sign_zero);
+                    SASSERT(s != sign_zero);
                     signs.push_back(s);
                 }
             }
@@ -2894,7 +2894,7 @@ namespace algebraic_numbers {
         m_imp->isolate_roots(p, x2v, roots);
     }
 
-    void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<polynomial::sign> & signs) {
+    void manager::isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<sign> & signs) {
         m_imp->isolate_roots(p, x2v, roots, signs);
     }
 
@@ -2952,7 +2952,7 @@ namespace algebraic_numbers {
         m_imp->inv(a);
     }
 
-    int manager::compare(numeral const & a, numeral const & b) {
+    sign manager::compare(numeral const & a, numeral const & b) {
         return m_imp->compare(const_cast<numeral&>(a), const_cast<numeral&>(b));
     }
 
@@ -3052,7 +3052,7 @@ namespace algebraic_numbers {
         l = rational(_l);
     }
 
-    polynomial::sign manager::eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
+    sign manager::eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v) {
         SASSERT(&(x2v.m()) == this);
         return m_imp->eval_sign_at(p, x2v);
     }
diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h
index 59e6401d7..2822f0042 100644
--- a/src/math/polynomial/algebraic_numbers.h
+++ b/src/math/polynomial/algebraic_numbers.h
@@ -173,7 +173,7 @@ namespace algebraic_numbers {
         /**
            \brief Isolate the roots of the given polynomial, and compute its sign between them.
         */
-        void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<polynomial::sign> & signs);
+        void isolate_roots(polynomial_ref const & p, polynomial::var2anum const & x2v, numeral_vector & roots, svector<sign> & signs);
 
         /**
            \brief Store in r the i-th root of p.
@@ -250,7 +250,7 @@ namespace algebraic_numbers {
            Return 0  if a == b
            Return 1  if a > b
         */
-        int compare(numeral const & a, numeral const & b);
+        sign compare(numeral const & a, numeral const & b);
         
         /**
            \brief a == b
@@ -304,7 +304,7 @@ namespace algebraic_numbers {
            Return 0                if p(alpha_1, ..., alpha_n) == 0
            Return positive number  if p(alpha_1, ..., alpha_n) >  0
         */
-        polynomial::sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v);
+        sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v);
 
         void get_polynomial(numeral const & a, svector<mpz> & r);
         
diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h
index 658d5de04..cf10dcd1a 100644
--- a/src/math/polynomial/polynomial.h
+++ b/src/math/polynomial/polynomial.h
@@ -30,6 +30,7 @@ Notes:
 #include "util/mpbqi.h"
 #include "util/rlimit.h"
 #include "util/lbool.h"
+#include "util/sign.h"
 
 class small_object_allocator;
 
@@ -44,12 +45,6 @@ namespace polynomial {
     typedef svector<var> var_vector;
     class monomial;
 
-    typedef enum { sign_neg = -1, sign_zero = 0, sign_pos = 1} sign;
-    inline sign operator-(sign s) { switch (s) { case sign_neg: return sign_pos; case sign_pos: return sign_neg; default: return sign_zero; } };
-    inline sign to_sign(int s) { return s == 0 ? sign_zero : (s > 0 ? sign_pos : sign_neg); }
-    inline sign operator*(sign a, sign b) { return to_sign((int)a * (int)b); }
-    inline bool is_zero(sign s) { return s == sign_zero; }
-
     int lex_compare(monomial const * m1, monomial const * m2);
     int lex_compare2(monomial const * m1, monomial const * m2, var min_var);
     int graded_lex_compare(monomial const * m1, monomial const * m2);
diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp
index 91744977e..6d6a3f09b 100644
--- a/src/math/polynomial/upolynomial.cpp
+++ b/src/math/polynomial/upolynomial.cpp
@@ -1327,25 +1327,25 @@ namespace upolynomial {
         div(sz, p, 2, two_x_1, buffer);
     }
 
-    polynomial::sign manager::sign_of(numeral const & c) {
+    sign manager::sign_of(numeral const & c) {
         if (m().is_zero(c))
-            return polynomial::sign_zero;
+            return sign_zero;
         if (m().is_pos(c))
-            return polynomial::sign_pos;
+            return sign_pos;
         else
-            return polynomial::sign_neg;
+            return sign_neg;
     }
 
     // Return the number of sign changes in the coefficients of p
     unsigned manager::sign_changes(unsigned sz, numeral const * p) {
         unsigned r = 0;
-        auto prev_sign = polynomial::sign_zero;
+        auto prev_sign = sign_zero;
         unsigned i = 0;
         for (; i < sz; i++) {
             auto sign = sign_of(p[i]);
-            if (sign == polynomial::sign_zero)
+            if (sign == sign_zero)
                 continue;
-            if (sign != prev_sign && prev_sign != polynomial::sign_zero)
+            if (sign != prev_sign && prev_sign != sign_zero)
                 r++;
             prev_sign = sign;
         }
@@ -1375,7 +1375,7 @@ namespace upolynomial {
         }
         return sign_changes(Q.size(), Q.c_ptr());
 #endif
-        polynomial::sign prev_sign = polynomial::sign_zero;
+        sign prev_sign = sign_zero;
         unsigned num_vars = 0;
         //   a0 a1     a2         a3
         //   a0 a0+a1  a0+a1+a2   a0+a1+a2+a3
@@ -1389,9 +1389,9 @@ namespace upolynomial {
                 m().add(Q[k], Q[k-1], Q[k]);
             }
             auto sign = sign_of(Q[k-1]);
-            if (polynomial::is_zero(sign))
+            if (::is_zero(sign))
                 continue;
-            if (sign != prev_sign && !polynomial::is_zero(prev_sign)) {
+            if (sign != prev_sign && !::is_zero(prev_sign)) {
                 num_vars++;
                 if (num_vars > 1)
                     return num_vars;
@@ -1729,14 +1729,14 @@ namespace upolynomial {
     }
 
     // Evaluate the sign of p(b)
-    polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpbq const & b) {
+    sign manager::eval_sign_at(unsigned sz, numeral const * p, mpbq const & b) {
         // Actually, given b = c/2^k, we compute the sign of (2^k)^n*p(b)
         // Original Horner Sequence
         //     ((a_n * b + a_{n-1})*b + a_{n-2})*b + a_{n-3} ...
         // Variation of the Horner Sequence for (2^k)^n*p(b)
         //     ((a_n * c + a_{n-1}*2_k)*c + a_{n-2}*(2_k)^2)*c + a_{n-3}*(2_k)^3 ... + a_0*(2_k)^n
         if (sz == 0)
-            return polynomial::sign_zero;
+            return sign_zero;
         if (sz == 1)
             return sign_of(p[0]);
         numeral const & c = b.numerator();
@@ -1762,14 +1762,14 @@ namespace upolynomial {
     }
 
     // Evaluate the sign of p(b)
-    polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpq const & b) {
+    sign manager::eval_sign_at(unsigned sz, numeral const * p, mpq const & b) {
         // Actually, given b = c/d, we compute the sign of (d^n)*p(b)
         // Original Horner Sequence
         //     ((a_n * b + a_{n-1})*b + a_{n-2})*b + a_{n-3} ...
         // Variation of the Horner Sequence for (d^n)*p(b)
         //     ((a_n * c + a_{n-1}*d)*c + a_{n-2}*d^2)*c + a_{n-3}*d^3 ... + a_0*d^n
         if (sz == 0)
-            return polynomial::sign_zero;
+            return sign_zero;
         if (sz == 1)
             return sign_of(p[0]);
         numeral const & c = b.numerator();
@@ -1796,11 +1796,11 @@ namespace upolynomial {
     }
 
     // Evaluate the sign of p(b)
-    polynomial::sign manager::eval_sign_at(unsigned sz, numeral const * p, mpz const & b) {
+    sign manager::eval_sign_at(unsigned sz, numeral const * p, mpz const & b) {
         // Using Horner Sequence
         //     ((a_n * b + a_{n-1})*b + a_{n-2})*b + a_{n-3} ...
         if (sz == 0)
-            return polynomial::sign_zero;
+            return sign_zero;
         if (sz == 1)
             return sign_of(p[0]);
         scoped_numeral r(m());
@@ -1817,21 +1817,21 @@ namespace upolynomial {
         return sign_of(r);
     }
 
-    polynomial::sign manager::eval_sign_at_zero(unsigned sz, numeral const * p) {
+    sign manager::eval_sign_at_zero(unsigned sz, numeral const * p) {
         if (sz == 0)
-            return polynomial::sign_zero;
+            return sign_zero;
         return sign_of(p[0]);
     }
 
-    polynomial::sign manager::eval_sign_at_plus_inf(unsigned sz, numeral const * p) {
+    sign manager::eval_sign_at_plus_inf(unsigned sz, numeral const * p) {
         if (sz == 0)
-            return polynomial::sign_zero;
+            return sign_zero;
         return sign_of(p[sz-1]);
     }
 
-    polynomial::sign manager::eval_sign_at_minus_inf(unsigned sz, numeral const * p) {
+    sign manager::eval_sign_at_minus_inf(unsigned sz, numeral const * p) {
         if (sz == 0)
-            return polynomial::sign_zero;
+            return sign_zero;
         unsigned degree = sz - 1;
         if (degree % 2 == 0)
             return sign_of(p[sz-1]);
@@ -2751,7 +2751,7 @@ namespace upolynomial {
        The arguments sign_a and sign_b must contain the values returned by
        eval_sign_at(sz, p, a) and eval_sign_at(sz, p, b).
     */
-    bool manager::refine_core(unsigned sz, numeral const * p, polynomial::sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b) {
+    bool manager::refine_core(unsigned sz, numeral const * p, sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b) {
         SASSERT(sign_a == eval_sign_at(sz, p, a));
         SASSERT(-sign_a == eval_sign_at(sz, p, b));
         SASSERT(sign_a != 0);
@@ -2759,7 +2759,7 @@ namespace upolynomial {
         bqm.add(a, b, mid);
         bqm.div2(mid);
         auto sign_mid = eval_sign_at(sz, p, mid);
-        if (polynomial::is_zero(sign_mid)) {
+        if (::is_zero(sign_mid)) {
             swap(mid, a);
             return false;
         }
@@ -2774,8 +2774,8 @@ namespace upolynomial {
 
     // See refine_core
     bool manager::refine(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b) {
-        polynomial::sign sign_a = eval_sign_at(sz, p, a);
-        SASSERT(!polynomial::is_zero(sign_a));
+        sign sign_a = eval_sign_at(sz, p, a);
+        SASSERT(!::is_zero(sign_a));
         return refine_core(sz, p, sign_a, bqm, a, b);
     }
 
@@ -2784,8 +2784,8 @@ namespace upolynomial {
     //
     // Return TRUE, if interval was squeezed, and new interval is stored in (a,b).
     // Return FALSE, if the actual root was found, it is stored in a.
-    bool manager::refine_core(unsigned sz, numeral const * p, polynomial::sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k) {
-        SASSERT(sign_a != polynomial::sign_zero);
+    bool manager::refine_core(unsigned sz, numeral const * p, sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k) {
+        SASSERT(sign_a != sign_zero);
         SASSERT(sign_a  == eval_sign_at(sz, p, a));
         SASSERT(-sign_a == eval_sign_at(sz, p, b));
         scoped_mpbq w(bqm);
@@ -2802,16 +2802,16 @@ namespace upolynomial {
     }
 
     bool manager::refine(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k) {
-        polynomial::sign sign_a = eval_sign_at(sz, p, a);
+        sign sign_a = eval_sign_at(sz, p, a);
         SASSERT(eval_sign_at(sz, p, b) == -sign_a);
         SASSERT(sign_a != 0);
         return refine_core(sz, p, sign_a, bqm, a, b, prec_k);
     }
 
     bool manager::convert_q2bq_interval(unsigned sz, numeral const * p, mpq const & a, mpq const & b, mpbq_manager & bqm, mpbq & c, mpbq & d) {
-        polynomial::sign sign_a = eval_sign_at(sz, p, a);
-        polynomial::sign sign_b = eval_sign_at(sz, p, b);
-        SASSERT(!polynomial::is_zero(sign_a) && !polynomial::is_zero(sign_b));
+        sign sign_a = eval_sign_at(sz, p, a);
+        sign sign_b = eval_sign_at(sz, p, b);
+        SASSERT(!::is_zero(sign_a) && !::is_zero(sign_b));
         SASSERT(sign_a == -sign_b);
         bool found_d = false;
         TRACE("convert_bug",
@@ -2843,7 +2843,7 @@ namespace upolynomial {
             SASSERT(bqm.lt(upper, b));
             while (true) {
                 auto sign_upper = eval_sign_at(sz, p, upper);
-                if (polynomial::is_zero(sign_upper)) {
+                if (::is_zero(sign_upper)) {
                     // found root
                     bqm.swap(c, upper);
                     bqm.del(lower); bqm.del(upper);
@@ -2887,8 +2887,8 @@ namespace upolynomial {
                 SASSERT(bqm.lt(lower, upper));
                 SASSERT(bqm.lt(lower, b));
                 while (true) {
-                    polynomial::sign sign_lower = eval_sign_at(sz, p, lower);
-                    if (polynomial::is_zero(sign_lower)) {
+                    sign sign_lower = eval_sign_at(sz, p, lower);
+                    if (::is_zero(sign_lower)) {
                         // found root
                         bqm.swap(c, lower);
                         bqm.del(lower); bqm.del(upper);
diff --git a/src/math/polynomial/upolynomial.h b/src/math/polynomial/upolynomial.h
index 348ccb271..6c52c0727 100644
--- a/src/math/polynomial/upolynomial.h
+++ b/src/math/polynomial/upolynomial.h
@@ -554,7 +554,7 @@ namespace upolynomial {
         numeral_vector    m_tr_tmp;
         numeral_vector    m_push_tmp;
 
-        polynomial::sign sign_of(numeral const & c);
+        sign sign_of(numeral const & c);
         struct drs_frame;
         void pop_top_frame(numeral_vector & p_stack, svector<drs_frame> & frame_stack);
         void push_child_frames(unsigned sz, numeral const * p, numeral_vector & p_stack, svector<drs_frame> & frame_stack);
@@ -735,32 +735,32 @@ namespace upolynomial {
         /**
            \brief Evaluate the sign of p(b) 
         */
-        polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpbq const & b);
+        sign eval_sign_at(unsigned sz, numeral const * p, mpbq const & b);
         
         /**
            \brief Evaluate the sign of p(b)
         */
-        polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpq const & b);
+        sign eval_sign_at(unsigned sz, numeral const * p, mpq const & b);
 
         /**
            \brief Evaluate the sign of p(b)
         */
-        polynomial::sign eval_sign_at(unsigned sz, numeral const * p, mpz const & b);
+        sign eval_sign_at(unsigned sz, numeral const * p, mpz const & b);
 
         /**
            \brief Evaluate the sign of p(0)
         */
-        polynomial::sign eval_sign_at_zero(unsigned sz, numeral const * p);
+        sign eval_sign_at_zero(unsigned sz, numeral const * p);
 
         /**
            \brief Evaluate the sign of p(+oo)
         */
-        polynomial::sign eval_sign_at_plus_inf(unsigned sz, numeral const * p);
+        sign eval_sign_at_plus_inf(unsigned sz, numeral const * p);
 
         /**
            \brief Evaluate the sign of p(-oo)
         */
-        polynomial::sign eval_sign_at_minus_inf(unsigned sz, numeral const * p);
+        sign eval_sign_at_minus_inf(unsigned sz, numeral const * p);
 
         /**
            \brief Evaluate the sign variations in the polynomial sequence at -oo
@@ -863,11 +863,11 @@ namespace upolynomial {
         // Return FALSE, if the actual root was found, it is stored in a.
         // 
         // See upolynomial.cpp for additional comments
-        bool refine_core(unsigned sz, numeral const * p, polynomial::sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b);
+        bool refine_core(unsigned sz, numeral const * p, sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b);
         
         bool refine(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b);
 
-        bool refine_core(unsigned sz, numeral const * p, polynomial::sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k);
+        bool refine_core(unsigned sz, numeral const * p, sign sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k);
         
         bool refine(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k);
         /////////////////////
diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp
index 081351f06..25013f6db 100644
--- a/src/nlsat/nlsat_evaluator.cpp
+++ b/src/nlsat/nlsat_evaluator.cpp
@@ -43,7 +43,7 @@ namespace nlsat {
             svector<section>   m_sections;
             unsigned_vector    m_sorted_sections; // refs to m_sections
             unsigned_vector    m_poly_sections;   // refs to m_sections
-            svector<polynomial::sign>  m_poly_signs;
+            svector<sign>  m_poly_signs;
             struct poly_info {
                 unsigned       m_num_roots;
                 unsigned       m_first_section;   // idx in m_poly_sections;
@@ -149,7 +149,7 @@ namespace nlsat {
                \brief Add polynomial with the given roots and signs.
             */
             unsigned_vector p_section_ids;
-            void add(anum_vector & roots, svector<polynomial::sign> & signs) {
+            void add(anum_vector & roots, svector<sign> & signs) {
                 p_section_ids.reset();
                 if (!roots.empty())
                     merge(roots, p_section_ids);
@@ -169,7 +169,7 @@ namespace nlsat {
             /**
                \brief Add constant polynomial 
             */
-            void add_const(polynomial::sign sign) {
+            void add_const(sign sign) {
                 unsigned first_sign    = m_poly_signs.size();
                 unsigned first_section = m_poly_sections.size();
                 m_poly_signs.push_back(sign);
@@ -226,12 +226,12 @@ namespace nlsat {
             }
             
             // Return the sign idx of pinfo
-            polynomial::sign sign(poly_info const & pinfo, unsigned i) const {
+            ::sign sign(poly_info const & pinfo, unsigned i) const {
                 return m_poly_signs[pinfo.m_first_sign + i];
             }
             
 #define LINEAR_SEARCH_THRESHOLD 8
-            polynomial::sign sign_at(unsigned info_id, unsigned c) const {
+            ::sign sign_at(unsigned info_id, unsigned c) const {
                 poly_info const & pinfo  = m_info[info_id];
                 unsigned num_roots = pinfo.m_num_roots;
                 if (num_roots < LINEAR_SEARCH_THRESHOLD) {
@@ -239,7 +239,7 @@ namespace nlsat {
                     for (; i < num_roots; i++) {
                         unsigned section_cell_id = cell_id(pinfo, i);
                         if (section_cell_id == c)
-                            return polynomial::sign_zero;
+                            return sign_zero;
                         else if (section_cell_id > c)
                             break;
                     }
@@ -253,7 +253,7 @@ namespace nlsat {
                     if (c < root_1_cell_id)
                         return sign(pinfo, 0);
                     else if (c == root_1_cell_id || c == root_n_cell_id)
-                        return polynomial::sign_zero;
+                        return sign_zero;
                     else if (c > root_n_cell_id)
                         return sign(pinfo, num_roots);
                     int low  = 0;
@@ -272,7 +272,7 @@ namespace nlsat {
                         SASSERT(low < mid && mid < high);
                         unsigned mid_cell_id = cell_id(pinfo, mid);
                         if (mid_cell_id == c) {
-                            return polynomial::sign_zero;
+                            return sign_zero;
                         }
                         if (c < mid_cell_id) {
                             high = mid;
@@ -381,7 +381,7 @@ namespace nlsat {
            
            \pre All variables of p are assigned in the current interpretation.
         */
-        polynomial::sign eval_sign(poly * p) {
+        sign eval_sign(poly * p) {
             // TODO: check if it is useful to cache results
             SASSERT(m_assignment.is_assigned(max_var(p)));
             return m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment);
@@ -449,7 +449,7 @@ namespace nlsat {
             return a->is_ineq_atom() ? eval_ineq(to_ineq_atom(a), neg) : eval_root(to_root_atom(a), neg);
         }
 
-        svector<polynomial::sign> m_add_signs_tmp;
+        svector<sign> m_add_signs_tmp;
         void add(poly * p, var x, sign_table & t) {
             SASSERT(m_pm.max_var(p) <= x);
             if (m_pm.max_var(p) < x) {
@@ -458,7 +458,7 @@ namespace nlsat {
             else {
                 // isolate roots of p
                 scoped_anum_vector & roots = m_add_roots_tmp;
-                svector<polynomial::sign> & signs = m_add_signs_tmp;
+                svector<sign> & signs = m_add_signs_tmp;
                 roots.reset();
                 signs.reset();
                 TRACE("nlsat_evaluator", tout << "x: " << x << " max_var(p): " << m_pm.max_var(p) << "\n";);
@@ -470,18 +470,18 @@ namespace nlsat {
         }
 
         // Evaluate the sign of p1^e1*...*pn^en (of atom a) in cell c of table t.
-        polynomial::sign sign_at(ineq_atom * a, sign_table const & t, unsigned c) const {
-            auto sign = polynomial::sign_pos;
+        sign sign_at(ineq_atom * a, sign_table const & t, unsigned c) const {
+            auto sign = sign_pos;
             unsigned num_ps = a->size();
             for (unsigned i = 0; i < num_ps; i++) {
-                polynomial::sign curr_sign = t.sign_at(i, c);
+                ::sign curr_sign = t.sign_at(i, c);
                 TRACE("nlsat_evaluator_bug", tout << "sign of i: " << i << " at cell " << c << "\n"; 
                       m_pm.display(tout, a->p(i)); 
                       tout << "\nsign: " << curr_sign << "\n";);
                 if (a->is_even(i) && curr_sign < 0)
-                    curr_sign = polynomial::sign_pos;
+                    curr_sign = sign_pos;
                 sign = sign * curr_sign;
-                if (sign == polynomial::sign_zero)
+                if (is_zero(sign)) 
                     break;
             }
             return sign;
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 0cafb4ac1..856089abe 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -208,7 +208,7 @@ namespace nlsat {
            \brief evaluate the given polynomial in the current interpretation.
            max_var(p) must be assigned in the current interpretation.
         */
-        polynomial::sign sign(polynomial_ref const & p) {
+        ::sign sign(polynomial_ref const & p) {
             SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p)));
             auto s = m_am.eval_sign_at(p, m_assignment);
             TRACE("nlsat_explain", tout << "p: " << p << " var: " << max_var(p) << " sign: " << s << "\n";);
@@ -271,7 +271,7 @@ namespace nlsat {
             polynomial_ref f(m_pm);
             for (unsigned i = 0; i < num_factors; i++) {
                 f = m_factors.get(i);
-                if (sign(f) == polynomial::sign_zero) {
+                if (is_zero(sign(f))) {
                     m_zero_fs.push_back(m_factors.get(i));
                     m_is_even.push_back(false);
                 } 
@@ -338,7 +338,7 @@ namespace nlsat {
                 lc = m_pm.coeff(p, x, k, reduct);
                 TRACE("nlsat_explain", tout << "lc: " << lc << " reduct: " << reduct << "\n";);
                 if (!is_zero(lc)) {
-                    if (sign(lc) != polynomial::sign_zero)
+                    if (!::is_zero(sign(lc))) 
                         return;
                     // lc is not the zero polynomial, but it vanished in the current interpretation.
                     // so we keep searching...
@@ -653,7 +653,7 @@ namespace nlsat {
                     TRACE("nlsat_explain", tout << "done, psc is a constant\n";);
                     return;
                 }
-                if (sign(s) == polynomial::sign_zero) {
+                if (is_zero(sign(s))) {
                     TRACE("nlsat_explain", tout << "psc vanished, adding zero assumption\n";);
                     add_zero_assumption(s);
                     continue;
@@ -1137,8 +1137,8 @@ namespace nlsat {
                 }
                 if (is_const(new_factor)) {
                     TRACE("nlsat_simplify_core", tout << "new factor is const\n";);
-                    polynomial::sign s = sign(new_factor); 
-                    if (s == polynomial::sign_zero) {
+                    auto s = sign(new_factor); 
+                    if (is_zero(s)) {
                         bool atom_val = a->get_kind() == atom::EQ;
                         bool lit_val  = l.sign() ? !atom_val : atom_val;
                         new_lit = lit_val ? true_literal : false_literal;
diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp
index c678f2b23..0957ac2cc 100644
--- a/src/nlsat/nlsat_interval_set.cpp
+++ b/src/nlsat/nlsat_interval_set.cpp
@@ -78,11 +78,11 @@ namespace nlsat {
             SASSERT(i.m_upper_open);
         }
         if (!i.m_lower_inf && !i.m_upper_inf) {
-            int s = am.compare(i.m_lower, i.m_upper);
+            auto s = am.compare(i.m_lower, i.m_upper);
             TRACE("nlsat_interval", tout << "lower: "; am.display_decimal(tout, i.m_lower); tout << ", upper: "; am.display_decimal(tout, i.m_upper);
                   tout << "\ns: " << s << "\n";);
             SASSERT(s <= 0);
-            if (s == 0) {
+            if (::is_zero(s)) {
                 SASSERT(!i.m_lower_open && !i.m_upper_open);
             }
         }
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index 8cbde38c5..fa6292c13 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -273,12 +273,7 @@ namespace qe {
         split_arith(lits, alits, uflits);
         auto avars = get_arith_vars(lits);
         vector<def> defs = arith_project(mdl, avars, alits);
-#if 0
-        prune_defs(defs);
-        substitute(defs, uflits);
-#else
         for (auto const& d : defs) uflits.push_back(m.mk_eq(d.var, d.term));
-#endif
         project_euf(mdl, uflits);
         lits.reset();
         lits.append(alits);
@@ -309,18 +304,6 @@ namespace qe {
     }
 
 
-    /**
-     * prune defs to only contain substitutions of terms with leading uninterpreted function.
-     */
-    void uflia_mbi::prune_defs(vector<def>& defs) {
-        unsigned i = 0; 
-        for (auto& d : defs) {
-            if (!is_shared(to_app(d.var)->get_decl())) {
-                defs[i++] = d;
-            }
-        }
-        defs.shrink(i);
-    }
 
     /**
        \brief add difference certificates to formula.
@@ -337,20 +320,6 @@ namespace qe {
         TRACE("qe", tout << "project: " << lits << "\n";);                
     }
 
-    /**
-     * \brief substitute solution to arithmetical variables into lits
-     */
-    void uflia_mbi::substitute(vector<def> const& defs, expr_ref_vector& lits) {
-        TRACE("qe", tout << "start substitute: " << lits << "\n";);        
-        for (auto const& def : defs) {
-            expr_safe_replace rep(m);
-            rep.insert(def.var, def.term);
-            rep(lits);
-            TRACE("qe", tout << "substitute: " << def.var << " |-> " << def.term << ": " << lits << "\n";);
-        }
-        IF_VERBOSE(1, verbose_stream() << "substituted: " << lits << "\n");
-    }
-
     /**
      * \brief project private symbols.
      */
diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h
index 97875993c..0c33c933e 100644
--- a/src/qe/qe_mbi.h
+++ b/src/qe/qe_mbi.h
@@ -122,12 +122,10 @@ namespace qe {
         void add_dcert(model_ref& mdl, expr_ref_vector& lits);
         app_ref_vector get_arith_vars(expr_ref_vector const& lits);
         vector<def> arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits);
-        void substitute(vector<def> const& defs, expr_ref_vector& lits);
         void project_euf(model_ref& mdl, expr_ref_vector& lits);
         void split_arith(expr_ref_vector const& lits, 
                          expr_ref_vector& alits,
                          expr_ref_vector& uflits);
-        void prune_defs(vector<def>& defs);
     public:
         uflia_mbi(solver* s, solver* emptySolver);
         ~uflia_mbi() override {}
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index b6c14c5d7..43ef8e6d1 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -1384,7 +1384,9 @@ namespace smt {
         }
 
         while (true) {
-            TRACE("unsat_core_bug", tout << consequent << ", idx: " << idx << " " << js.get_kind() << "\n";);
+            TRACE("unsat_core_trail", tout << consequent << ", idx: " << idx << " " << js.get_kind() << "\n";
+                  m_ctx.display_literal_smt2(tout, consequent) << "\n";
+                  );
             switch (js.get_kind()) {
             case b_justification::CLAUSE: {
                 clause * cls = js.get_clause();
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 9b58d8363..9d26b10dc 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1992,7 +1992,9 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
         seq = mk_concat(elems.size(), elems.c_ptr());
     }
     TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";);
-    add_axiom(~mk_eq(len_e, m_autil.mk_numeral(lo, true), false), mk_seq_eq(seq, e));
+    literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false);
+    literal b = mk_seq_eq(seq, e);
+    add_axiom(~a, b);
     if (!ctx.at_base_level()) {
         m_trail_stack.push(push_replay(alloc(replay_fixed_length, m, len_e)));
     }
@@ -3398,6 +3400,7 @@ bool theory_seq::solve_ne(unsigned idx) {
 
             dependency* deps1 = nullptr;
             if (explain_eq(n.l(), n.r(), deps1)) {
+                std::cout << "updated explain\n";
                 literal diseq = mk_eq(n.l(), n.r(), false);
                 if (ctx.get_assignment(diseq) == l_false) {
                     new_lits.reset();                
@@ -5647,6 +5650,10 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
     if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); push_lit_as_expr(l4, exprs); }
     if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); push_lit_as_expr(l5, exprs); }
     TRACE("seq", ctx.display_literals_verbose(tout << "assert:", lits) << "\n";);
+    
+    IF_VERBOSE(10, verbose_stream() << "ax ";
+               for (literal l : lits) ctx.display_literal_smt2(verbose_stream() << " ", l); 
+               verbose_stream() << "\n");
     m_new_propagation = true;
     ++m_stats.m_add_axiom;
     
@@ -6329,7 +6336,7 @@ void theory_seq::add_unit_axiom(expr* n) {
     expr* u = nullptr;
     VERIFY(m_util.str.is_unit(n, u));
     sort* s = m.get_sort(u);
-    expr_ref rhs(mk_skolem(symbol("inv-unit"), n, nullptr, nullptr, nullptr, s), m);
+    expr_ref rhs(mk_skolem(symbol("seq.inv-unit"), n, nullptr, nullptr, nullptr, s), m);
     add_axiom(mk_eq(u, rhs, false));
 }
 
diff --git a/src/util/sign.h b/src/util/sign.h
new file mode 100644
index 000000000..8352300ec
--- /dev/null
+++ b/src/util/sign.h
@@ -0,0 +1,24 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    sign.h
+
+Abstract:
+
+    Sign
+
+Author:
+
+    Nikolaj Bjorner
+
+--*/
+
+#pragma once
+
+typedef enum { sign_neg = -1, sign_zero = 0, sign_pos = 1} sign;
+inline sign operator-(sign s) { switch (s) { case sign_neg: return sign_pos; case sign_pos: return sign_neg; default: return sign_zero; } };
+inline sign to_sign(int s) { return s == 0 ? sign_zero : (s > 0 ? sign_pos : sign_neg); }
+inline sign operator*(sign a, sign b) { return to_sign((int)a * (int)b); }
+inline bool is_zero(sign s) { return s == sign_zero; }