fixes and checks

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Mar 5, 2024 · d7e419b · d7e419b
1 parent ab0459e
commit d7e419b
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 5 deletions.
diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp
@@ -171,6 +171,7 @@ namespace bv {
         }
         else {
             m_eval.repair_up(e);
+            SASSERT(eval_is_correct(e));
             for (auto p : m_terms.parents(e))
                 m_repair_up.insert(p->get_id());
         }
@@ -191,8 +192,17 @@ namespace bv {
         model_ref mdl = alloc(model, m);
         auto& terms = m_eval.sort_assertions(m_terms.assertions());
         for (expr* e : terms) {
+            if (!eval_is_correct(to_app(e))) {
+                verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
+                if (bv.is_bv(e)) {
+                    auto const& v0 = m_eval.wval0(e);
+                    auto const& v1 = m_eval.wval1(to_app(e));
+                    verbose_stream() << v0 << "\n" << v1 << "\n";
+                }
+            }
             if (!is_uninterp_const(e))
                 continue;
+
             auto f = to_app(e)->get_decl();
             if (m.is_bool(e))
                 mdl->register_decl(f, m.mk_bool_val(m_eval.bval0(e)));

diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
@@ -1020,7 +1020,7 @@ namespace bv {
         unsigned parity_e = e.parity(e.bits);
         unsigned parity_b = b.parity(b.bits);
 
-#if 0
+#if 1
 
         auto& x = m_tmp;
         auto& y = m_tmp2;
@@ -1521,9 +1521,9 @@ namespace bv {
     }
 
     bool sls_eval::try_repair_extract(bvval const& e, bvval& a, unsigned lo) {
-        for (unsigned i = 0; i < a.bw; ++i)
-            if (!a.get(a.fixed, i))
-                a.set(a.bits, i, e.get(e.bits, i + lo));
+        for (unsigned i = 0; i < e.bw; ++i)
+            if (!a.get(a.fixed, i + lo))
+                a.set(a.bits, i + lo, e.get(e.bits, i));
         return true;
     }
 
@@ -1553,6 +1553,6 @@ namespace bv {
         if (m.is_bool(e))
             set(e, bval1(to_app(e)));
         else if (bv.is_bv(e)) 
-            wval0(e).try_set(wval1(to_app(e)));        
+            wval0(e).set(wval1(to_app(e)));        
     }
 }