diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index ce8fc3e9d..ae052231c 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -30,5 +30,173 @@ namespace arith {
         add_clause(eqz, eq);
     }
 
+    // to_int (to_real x) = x
+    // to_real(to_int(x)) <= x < to_real(to_int(x)) + 1
+    void solver::mk_to_int_axiom(app* n) {
+        expr* x = nullptr, *y = nullptr;
+        VERIFY (a.is_to_int(n, x));            
+        if (a.is_to_real(x, y)) {
+            literal eq = eq_internalize(y, n);
+            add_clause(eq);
+        }
+        else {
+            expr_ref to_r(a.mk_to_real(n), m);
+            expr_ref lo(a.mk_le(a.mk_sub(to_r, x), a.mk_real(0)), m);
+            expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m);
+            literal llo = b_internalize(lo);
+            literal lhi = b_internalize(hi);
+            add_clause(llo);
+            add_clause(~lhi);
+        }
+    }
+
+    // is_int(x) <=> to_real(to_int(x)) = x
+    void solver::mk_is_int_axiom(app* n) {
+        expr* x = nullptr;
+        VERIFY(a.is_is_int(n, x));
+        expr_ref lhs(a.mk_to_real(a.mk_to_int(x)), m);
+        literal eq = eq_internalize(lhs, x);
+        literal is_int = ctx.expr2literal(n);
+        add_equiv(is_int, eq);
+    }
+
+
+#if 0
+
+
+    void mk_ite_axiom(expr* n) {
+        return;
+        expr* c = nullptr, *t = nullptr, *e = nullptr;
+        VERIFY(m.is_ite(n, c, t, e));
+        literal e1 = th.mk_eq(n, t, false);
+        literal e2 = th.mk_eq(n, e, false);
+        scoped_trace_stream sts(th, e1, e2);
+        mk_axiom(e1, e2);
+    }
+
+
+    // create axiom for 
+    //    u = v + r*w,
+    ///   abs(r) > r >= 0
+    void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r) {
+        app_ref term(m);
+        term = a.mk_mul(a.mk_numeral(r, true), get_enode(w)->get_owner());
+        term = a.mk_add(get_enode(v)->get_owner(), term);
+        term = a.mk_sub(get_enode(u)->get_owner(), term);
+        theory_var z = internalize_def(term);
+        lpvar zi = register_theory_var_in_lar_solver(z);
+        lpvar vi = register_theory_var_in_lar_solver(v);
+        add_def_constraint_and_equality(zi, lp::GE, rational::zero());
+        add_def_constraint_and_equality(zi, lp::LE, rational::zero());
+        add_def_constraint_and_equality(vi, lp::GE, rational::zero());
+        add_def_constraint_and_equality(vi, lp::LT, abs(r));
+        SASSERT(!is_infeasible());
+        TRACE("arith", tout << term << "\n" << lp().constraints(););
+    }
+
+    void mk_idiv_mod_axioms(expr * p, expr * q) {
+        if (a.is_zero(q)) {
+            return;
+        }
+        TRACE("arith", tout << expr_ref(p, m) << " " << expr_ref(q, m) << "\n";);
+        // if q is zero, then idiv and mod are uninterpreted functions.
+        expr_ref div(a.mk_idiv(p, q), m);
+        expr_ref mod(a.mk_mod(p, q), m);
+        expr_ref zero(a.mk_int(0), m);
+        if (a.is_zero(p)) {
+            // q != 0 => (= (div 0 q) 0)
+            // q != 0 => (= (mod 0 q) 0)
+            literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
+            literal q_le_0 = mk_literal(a.mk_le(q, zero));
+            literal d_ge_0 = mk_literal(a.mk_ge(div, zero));
+            literal d_le_0 = mk_literal(a.mk_le(div, zero));
+            literal m_ge_0 = mk_literal(a.mk_ge(mod, zero));
+            literal m_le_0 = mk_literal(a.mk_le(mod, zero));
+            mk_axiom(q_ge_0, d_ge_0);
+            mk_axiom(q_ge_0, d_le_0);
+            mk_axiom(q_ge_0, m_ge_0);
+            mk_axiom(q_ge_0, m_le_0);
+            mk_axiom(q_le_0, d_ge_0);
+            mk_axiom(q_le_0, d_le_0);
+            mk_axiom(q_le_0, m_ge_0);
+            mk_axiom(q_le_0, m_le_0);
+            return;
+        }
+#if 0
+        expr_ref eqr(m.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p), m);
+        ctx().get_rewriter()(eqr);
+        literal eq = mk_literal(eqr);
+#else
+        literal eq         = th.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p, false);
+#endif
+        literal mod_ge_0   = mk_literal(a.mk_ge(mod, zero));
+
+        rational k(0);
+        expr_ref upper(m);
+
+        if (a.is_numeral(q, k)) {
+            if (k.is_pos()) { 
+                upper = a.mk_numeral(k - 1, true);
+            }
+            else if (k.is_neg()) {
+                upper = a.mk_numeral(-k - 1, true);
+            }
+        }
+        else {
+            k = rational::zero();
+        }
+
+        context& c = ctx();
+        if (!k.is_zero()) {
+            mk_axiom(eq);
+            mk_axiom(mod_ge_0);
+            mk_axiom(mk_literal(a.mk_le(mod, upper)));
+            {
+                std::function<void(void)> log = [&,this]() {
+                    th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
+                    th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())));
+                    th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper)));
+                };
+                if_trace_stream _ts(m, log);
+            }
+        }
+        else {
+
+            /*literal div_ge_0   = */ mk_literal(a.mk_ge(div, zero));
+            /*literal div_le_0   = */ mk_literal(a.mk_le(div, zero));
+            /*literal p_ge_0     = */ mk_literal(a.mk_ge(p, zero));
+            /*literal p_le_0     = */ mk_literal(a.mk_le(p, zero));
+
+            // q >= 0 or p = (p mod q) + q * (p div q)
+            // q <= 0 or p = (p mod q) + q * (p div q)
+            // q >= 0 or (p mod q) >= 0
+            // q <= 0 or (p mod q) >= 0
+            // q <= 0 or (p mod q) <  q
+            // q >= 0 or (p mod q) < -q
+            literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
+            literal q_le_0 = mk_literal(a.mk_le(q, zero));
+
+            mk_axiom(q_ge_0, eq);
+            mk_axiom(q_le_0, eq);
+            mk_axiom(q_ge_0, mod_ge_0);
+            mk_axiom(q_le_0, mod_ge_0);
+            mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));            
+            mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));        
+
+        }
+        if (params().m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
+            unsigned _k = k.get_unsigned();
+            literal_buffer lits;
+            expr_ref_vector exprs(m);
+            for (unsigned j = 0; j < _k; ++j) {
+                literal mod_j = th.mk_eq(mod, a.mk_int(j), false);
+                lits.push_back(mod_j);
+                exprs.push_back(c.bool_var2expr(mod_j.var()));
+                ctx().mark_as_relevant(mod_j);
+            }
+            ctx().mk_th_axiom(get_id(), lits.size(), lits.begin());                
+        }            
+    }
+#endif
 
 }
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 44cd0702b..19845c28b 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -52,6 +52,8 @@ namespace arith {
 
         // axioms
         void mk_div_axiom(expr* p, expr* q);
+        void solver::mk_to_int_axiom(app* n);
+        void mk_is_int_axiom(app* n);
 
         void pop_core(unsigned n) override;
         
diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
index bc9b8b385..a7182f996 100644
--- a/src/smt/smt_theory.h
+++ b/src/smt/smt_theory.h
@@ -18,6 +18,7 @@ Revision History:
 --*/
 #pragma once
 
+#include "ast/ast_pp.h"
 #include "smt/smt_enode.h"
 #include "smt/smt_quantifier.h"
 #include "util/obj_hashtable.h"
@@ -527,7 +528,7 @@ namespace smt {
             ast_manager& m = get_manager();
             if (lhs->get_id() > rhs->get_id())
                 std::swap(lhs, rhs);
-            if (m.are_distinct(lhs, rhs))
+            if (m.are_distinct(lhs, rhs))                
                 return m.mk_false();
             if (m.are_equal(lhs, rhs))
                 return m.mk_true();
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 20ea39272..f3ff4534a 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -279,9 +279,10 @@ namespace smt {
         if (opt_VerifyFinalCheckProgress) {
             finalCheckProgressIndicator = true;
         }
-
-        if (get_manager().is_true(_e)) return;
         ast_manager& m = get_manager();
+        SASSERT(!m.is_true(_e));
+
+        if (m.is_true(_e)) return;
         TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;);
         expr_ref e(_e, m);
         //th_rewriter rw(m);
@@ -1974,7 +1975,7 @@ namespace smt {
                 // inconsistency check: value
                 if (!can_two_nodes_eq(eqc_nn1, eqc_nn2)) {
                     TRACE("str", tout << "inconsistency detected: " << mk_pp(eqc_nn1, m) << " cannot be equal to " << mk_pp(eqc_nn2, m) << std::endl;);
-                    expr_ref to_assert(mk_not(m, ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m);
+                    expr_ref to_assert(mk_not(m, m.mk_eq(eqc_nn1, eqc_nn2)), m);
                     assert_axiom(to_assert);
                     // this shouldn't use the integer theory at all, so we don't allow the option of quick-return
                     return false;