From b02c69828419e792c67876f7beecfabe73196aac Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 8 Nov 2018 16:52:10 -0800
Subject: [PATCH] align variable names with dimacs input

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/mk_util.py                |  4 ----
 src/api/api_solver.cpp            |  3 +++
 src/ast/rewriter/seq_rewriter.cpp |  6 +++++-
 src/tactic/fpa/qffp_tactic.cpp    | 13 +++++++------
 4 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 6372e87fc..08ff771e7 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1859,14 +1859,11 @@ class DotNetCoreDLLComponent(Component):
         if not is_dotnet_core_enabled():
             return
         cs_fp_files = []
-        cs_files    = []
         for cs_file in get_cs_files(self.src_dir):
             cs_fp_files.append(os.path.join(self.to_src_dir, cs_file))
-            cs_files.append(cs_file)
         if self.assembly_info_dir != '.':
             for cs_file in get_cs_files(os.path.join(self.src_dir, self.assembly_info_dir)):
                 cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file))
-                cs_files.append(os.path.join(self.assembly_info_dir, cs_file))
         dllfile = '%s.dll' % self.dll_name
         out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name))
         for cs_file in cs_fp_files:
@@ -1874,7 +1871,6 @@ class DotNetCoreDLLComponent(Component):
             out.write(cs_file)
         out.write('\n')
 
-        # TBD: can this be replaced by running "dotnet new classlib"?
         csproj = os.path.join(self.to_src_dir, "core", "core.csproj")
         dotnetCmdLine = [DOTNET, "build", csproj]
         
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 204370346..cb4ae19db 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -188,6 +188,9 @@ extern "C" {
             sat2goal s2g;
             ref<sat2goal::mc> mc;
             atom2bool_var a2b(m);
+            for (unsigned v = 0; v < solver.num_vars(); ++v) {
+                a2b.insert(m.mk_const(symbol(v), m.mk_bool_sort()), v);
+            }
             goal g(m);            
             s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc);
             for (unsigned i = 0; i < g.size(); ++i) {
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index e4ad3bb9d..dad485d94 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -844,6 +844,10 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
     return BR_FAILED;
 }
 
+//  (str.replace s t t') is the string obtained by replacing the first occurrence 
+//  of t in s, if any, by t'. Note that if t is empty, the result is to prepend
+//  t' to s; also, if t does not occur in s then the result is s.
+
 br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result) {
     zstring s1, s2, s3;
     if (m_util.str.is_string(a, s1) && m_util.str.is_string(b, s2) && 
@@ -855,7 +859,7 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
         result = a;
         return BR_DONE;
     }
-    if (m_util.str.is_string(b, s2) && s2.length() == 0) {
+    if (m_util.str.is_empty(b)) {
         result = m_util.str.mk_concat(c, a);
         return BR_REWRITE1;
     }
diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp
index 9f4f1b604..97f05c17b 100644
--- a/src/tactic/fpa/qffp_tactic.cpp
+++ b/src/tactic/fpa/qffp_tactic.cpp
@@ -17,15 +17,16 @@ Notes:
 
 --*/
 #include "tactic/tactical.h"
-#include "tactic/core/simplify_tactic.h"
-#include "tactic/bv/bit_blaster_tactic.h"
-#include "sat/tactic/sat_tactic.h"
 #include "tactic/fpa/fpa2bv_tactic.h"
-#include "smt/tactic/smt_tactic.h"
+#include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
-#include "ackermannization/ackermannize_bv_tactic.h"
 #include "tactic/arith/probe_arith.h"
+#include "tactic/bv/bit_blaster_tactic.h"
 #include "tactic/smtlogics/qfnra_tactic.h"
+#include "sat/tactic/sat_tactic.h"
+#include "sat/sat_solver/inc_sat_solver.h"
+#include "smt/tactic/smt_tactic.h"
+#include "ackermannization/ackermannize_bv_tactic.h"
 
 #include "tactic/fpa/qffp_tactic.h"
 
@@ -95,7 +96,7 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
                            cond(mk_is_propositional_probe(),
                                 cond(mk_produce_proofs_probe(),
                                      mk_smt_tactic(m, p), // `sat' does not support proofs.
-                                     mk_sat_tactic(m, p)),
+                                     mk_psat_tactic(m, p)),
                                 cond(mk_is_fp_qfnra_probe(),
                                      mk_qfnra_tactic(m, p),
                                      mk_smt_tactic(m, p))));