fix #7454

Z3Prover · Nov 17, 2024 · 2310514 · 2310514
1 parent 5fd1231
commit 2310514
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
@@ -150,6 +150,8 @@ void bv_decl_plugin::finalize() {
 }
 
 void bv_decl_plugin::mk_bv_sort(unsigned bv_size) {
+    if (bv_size + 1 == 0)
+        throw default_exception("bit-vector of size 2^32-1 are not supported");
     force_ptr_array_size(m_bv_sorts, bv_size + 1);
     if (!m_bv_sorts[bv_size]) {
         parameter p(bv_size);

diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp
@@ -255,9 +255,12 @@ namespace sls {
     }
 
     void smt_plugin::sls_phase_to_smt() {
+        if (!m_has_new_sls_phase)
+            return;
         IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase\n");
         for (auto v : m_shared_bool_vars) 
-            ctx.force_phase(sat::literal(v, !m_sls_phase[v]));        
+            ctx.force_phase(sat::literal(v, !m_sls_phase[v]));
+        m_has_new_sls_phase = false;
     }
 
     void smt_plugin::sls_activity_to_smt() {
@@ -347,6 +350,7 @@ namespace sls {
             expr_ref val(tr(sync_val), m);
             ctx.set_value(t, val);
         }
+        m_has_new_sls_values = false;
     }
 
     void smt_plugin::add_shared_term(expr* t) {