diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp
index d9858b3c1..6eb697880 100644
--- a/src/qe/qe_sat_tactic.cpp
+++ b/src/qe/qe_sat_tactic.cpp
@@ -672,9 +672,9 @@ namespace qe {
             lbool r = solver.check();
             m_assignments.reset();
             solver.get_assignments(m_assignments);
+            if(r == l_true && i == 0) solver.get_model(model);
             solver.pop(1);
-            check_success(r != l_undef);
-            if (r == l_true && i == 0) solver.get_model(model);
+            check_success(r != l_undef);            
             return r == l_true;
         }
 
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 3442cd369..b8034b19d 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -529,6 +529,7 @@ namespace smt {
 
     bool theory_bv::get_fixed_value(app* x, numeral & result) const {
         context& ctx = get_context();
+        CTRACE("bv", !ctx.e_internalized(x), tout << "not internalized " << mk_pp(x, get_manager()) << "\n";);
         if (!ctx.e_internalized(x)) return false;
         enode * e    = ctx.get_enode(x);
         theory_var v = e->get_th_var(get_id());