build fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Nov 15, 2024 · 3f40798 · 3f40798
1 parent ca6ec0d
commit 3f40798
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 9 deletions.
diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
@@ -790,17 +790,16 @@ class seq_expr_inverter : public iexpr_inverter {
                 r = m.mk_or(r, emp);
                 return true;
             }
-            if (uncnstr(args[1])) {
+            if (uncnstr(args[1]) && seq.is_string(args[0]->get_sort())) {
                 // x contains y -> r
-                // y -> if r then x else x + x
+                // y -> if r then x else x + x + a
                 mk_fresh_uncnstr_var_for(f, r);
                 if (m_mc)
-                    add_def(args[1], m.mk_ite(r, args[0], seq.str.mk_concat(args[0], args[0])));
+                    add_def(args[1], m.mk_ite(r, args[0], seq.str.mk_concat(args[0], args[0], seq.str.mk_string(zstring("a")))));
                 return true;
             }
             return false;
         default:
-            verbose_stream() << f->get_name() << "\n";
             return false;                
 
         }

diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h
@@ -33,7 +33,7 @@ namespace sls {
         virtual void set_value(expr* t, expr* v) = 0;
         virtual void force_phase(sat::literal lit) = 0;
         virtual void set_has_new_best_phase(bool b) = 0;
-        virtual bool get_value(expr* v, expr_ref& val) = 0;
+        virtual bool get_smt_value(expr* v, expr_ref& val) = 0;
         virtual bool get_best_phase(sat::bool_var v) = 0;
         virtual expr* bool_var2expr(sat::bool_var v) = 0;
         virtual void inc_activity(sat::bool_var v, double inc) = 0;

diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h
@@ -101,10 +101,10 @@ namespace sls {
         void inc_activity(sat::bool_var v, double inc) override {}
         unsigned get_num_bool_vars() const override;
         bool parallel_mode() const override { return false; }
-        bool get_value(expr* v, expr_ref& value) override { return false; }
+        bool get_smt_value(expr* v, expr_ref& value) override { return false; }
 
     };
 
 }
 
-#endif
+#endif
diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h
@@ -110,8 +110,9 @@ namespace smt {
         void set_finished() override;
         unsigned get_num_bool_vars() const override;
         void inc_activity(sat::bool_var v, double inc) override;
-        bool parallel_mode() const { return m_parallel_mode; }
-        bool get_value(expr* v, expr_ref& value) override;
+        bool parallel_mode() const override { return m_parallel_mode; }
+        bool get_smt_value(expr* v, expr_ref& value) override;
+
     };
 
 }