diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 0f426b6fd..c67cc6ad1 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1705,6 +1705,7 @@ namespace pdr {
     void context::create_children(model_node& n) {        
         SASSERT(n.level() > 0);
         bool use_model_generalizer = m_params.get_bool(":use-model-generalizer", false);
+        datalog::scoped_no_proof _sc(m);
  
         pred_transformer& pt = n.pt();
         model_ref M = n.get_model_ptr();
@@ -1764,12 +1765,13 @@ namespace pdr {
         if (!vars.empty()) {
             // also fresh names for auxiliary variables in body?
             expr_substitution sub(m);
+            expr_ref_vector refs(m);
             expr_ref tmp(m);
             proof_ref pr(m);
             pr = m.mk_asserted(m.mk_true());
-
             for (unsigned i = 0; i < vars.size(); ++i) {                
-                M->eval(vars[i]->get_decl(), tmp);                
+                VERIFY (M->eval(vars[i].get(), tmp, true));                
+                refs.push_back(tmp);
                 sub.insert(vars[i].get(), tmp, pr);
             }
             if (!rep) rep = mk_expr_simp_replacer(m);
diff --git a/src/muz_qe/qe_arith_plugin.cpp b/src/muz_qe/qe_arith_plugin.cpp
index c10716dc8..14cb5ee53 100644
--- a/src/muz_qe/qe_arith_plugin.cpp
+++ b/src/muz_qe/qe_arith_plugin.cpp
@@ -1863,11 +1863,18 @@ public:
                 // x := coeff * x + s
                 def = m_util.mk_add(m_util.mk_mul(x_t.get_coeff(), def), x_t.get_term());
             }
+            if (is_strict) {
+                SASSERT(m_util.m_arith.is_real(x));
+                // We actually want a supremum, such that dual inequalities are satisfied.
+                // i.e. for every dual inequality , if the dual bound is feasible, make sure to
+                // choose a value in the feasible range.
+                def = m_util.mk_sub(def, m_util.mk_one(x));
+            }
 
             m_util.simplify(def);
 
 
-            TRACE("qe", tout << "TBD: " << a << " " << mk_pp(def, m) << "\n";);
+            TRACE("qe", tout << "TBD (for Real): " << a << " " << mk_pp(def, m) << "\n";);
         }
 
         expr_ref mk_not(expr* e) {