diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 5bc0b1836..1acbb592b 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -1257,7 +1257,6 @@ namespace opt {
         }
         def result;
         if (compute_def) {
-            TRACE("opt1", tout << m_rows[row_id1] << "\n";);
             result = def(m_rows[row_id1], x);
             m_var2value[x] = eval(result);
             TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 23276a3f1..5769340ee 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -51,7 +51,7 @@ namespace q {
                 for (expr* e : exp) {
                     sat::literal lit = ctx.internalize(e, l.sign(), false, false); 
                     add_clause(~l, lit);                    
-                    ctx.add_aux(~l, lit);
+                    ctx.add_root(~l, lit);
                 }
             }
             else {