diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java
index 667c91a53..5ce5a584a 100644
--- a/src/api/java/InterpolationContext.java
+++ b/src/api/java/InterpolationContext.java
@@ -90,7 +90,7 @@ public class InterpolationContext extends Context
     public class ComputeInterpolantResult 
     {
         public Z3_lbool status = Z3_lbool.Z3_L_UNDEF;
-        public ASTVector interp = null;
+        public BoolExpr[] interp = null;
         public Model model = null;
     };
     
@@ -109,8 +109,13 @@ public class InterpolationContext extends Context
         ComputeInterpolantResult res = new ComputeInterpolantResult();
         Native.LongPtr n_i = new Native.LongPtr();
         Native.LongPtr n_m = new Native.LongPtr();
-        res.status =Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
-        if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value);
+        res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
+        if (res.status == Z3_lbool.Z3_L_FALSE) {xx
+	    res.interp = new BoolExpr[Native.astVectorSize(nCtx(), n_i.value)];
+	    for (int i = 0; i < res.interp.Length; ++i) {
+		res.interp[i] = new BoolExpr(this, Native.astVectorGet(nCtx(), i));
+	    }
+	}
         if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
         return res;
     }
diff --git a/src/math/euclid/euclidean_solver.cpp b/src/math/euclid/euclidean_solver.cpp
index 02ff1591e..9225a87ee 100644
--- a/src/math/euclid/euclidean_solver.cpp
+++ b/src/math/euclid/euclidean_solver.cpp
@@ -609,6 +609,7 @@ struct euclidean_solver::imp {
             // neg coeffs... to make sure that m_next_x is -1
             neg_coeffs(eq.m_as);
             neg_coeffs(eq.m_bs);
+            m().neg(eq.m_c);
         }
         unsigned sz = eq.size();
         for (unsigned i = 0; i < sz; i++) {
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 74f2e09fa..4f810727a 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1411,6 +1411,10 @@ namespace smt {
     
     void context::mk_th_axiom(theory_id tid, unsigned num_lits, literal * lits, unsigned num_params, parameter * params) {
         justification * js = 0; 
+        TRACE("mk_th_axiom", 
+              display_literals_verbose(tout, num_lits, lits);
+              tout << "\n";);
+
         if (m_manager.proofs_enabled()) {
             js = mk_justification(theory_axiom_justification(tid, m_region, num_lits, lits, num_params, params));
         }
@@ -1425,13 +1429,11 @@ namespace smt {
     
     void context::mk_th_axiom(theory_id tid, literal l1, literal l2, unsigned num_params, parameter * params) {
         literal ls[2] = { l1, l2 };
-        TRACE("mk_th_axiom", display_literal(tout, l1); tout << " "; display_literal(tout, l2); tout << "\n";);
         mk_th_axiom(tid, 2, ls, num_params, params);
     }
 
     void context::mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params, parameter * params) {
         literal ls[3] = { l1, l2, l3 };
-        TRACE("mk_th_axiom", display_literal(tout, l1); tout << " "; display_literal(tout, l2); tout << " "; display_literal(tout, l3); tout << "\n";);
         mk_th_axiom(tid, 3, ls, num_params, params);
     }
 
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index f481e35d0..d0c9953c2 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -439,6 +439,7 @@ namespace smt {
                     j += rational(1);
                 }
                 ctx.mk_th_axiom(get_id(), lits.size(), lits.begin());
+                
 #else
                 // performs slightly worse.
                 literal_buffer lits;
@@ -2788,6 +2789,7 @@ namespace smt {
               tout << " --> ";
               ctx.display_detailed_literal(tout, l); 
               tout << "\n";);
+        SASSERT(false);
         if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) {
             literal_vector & lits = m_tmp_literal_vector2;
             lits.reset();
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 45c615e0c..d34b02a27 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -1061,6 +1061,7 @@ namespace smt {
                 }
                 if (!failed) {
                     m_solver.assert_eq(as.size(), as.c_ptr(), xs.c_ptr(), c, j);
+                    TRACE("euclidean_solver", tout << "add definition: v" << v << " := " << mk_ismt2_pp(n, t.get_manager()) << "\n";);
                 }
                 else {
                     TRACE("euclidean_solver", tout << "failed for:\n" << mk_ismt2_pp(n, t.get_manager()) << "\n";);
@@ -1191,7 +1192,8 @@ namespace smt {
                 if (l != 0) {
                     rational l_old = l->get_value().get_rational().to_rational();
                     rational l_new = g*ceil((l_old - c2)/g) + c2;
-                    TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n";);
+                    TRACE("euclidean_solver_new", tout << "new lower: " << l_new << " old: " << l_old << "\n";
+                          tout << "c: " << c2 << " ceil((l_old - c2)/g): " << (ceil((l_old - c2)/g)) << "\n";);
                     if (l_new > l_old) {
                         propagated = true;
                         mk_lower(v, l_new, l, m_js);