From 23a74b3c265d2ea5be7c1d9067c908cce386d0f0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 23 Apr 2014 08:07:37 +0200
Subject: [PATCH] fix assertions reported by Christoph

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3.py        | 16 ++++++++++++++++
 src/opt/opt_sls_solver.h    |  1 -
 src/opt/pb_sls.cpp          |  7 +++++--
 src/opt/weighted_maxsat.cpp |  1 -
 4 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 3145dc75a..d31bcb729 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -6010,6 +6010,22 @@ class Solver(Z3PPObject):
         """
         return Z3_solver_to_string(self.ctx.ref(), self.solver)
 
+    def to_smt2(self):
+	"""return SMTLIB2 formatted benchmark for solver's assertions"""
+	es = self.assertions()
+	sz = len(es)
+	sz1 = sz
+	if sz1 > 0:
+	    sz1 -= 1
+	v = (Ast * sz1)()
+	for i in range(sz1):
+	    v[i] = es[i].as_ast()
+	if sz > 0:
+	    e = es[sz1].as_ast()
+	else:
+	    e = BoolVal(True, self.ctx).as_ast()
+	return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
+
 def SolverFor(logic, ctx=None):
     """Create a solver customized for the given logic. 
 
diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h
index 7ed4c40a6..cd634e728 100644
--- a/src/opt/opt_sls_solver.h
+++ b/src/opt/opt_sls_solver.h
@@ -90,7 +90,6 @@ namespace opt {
             m_solver->get_labels(r);
         }
         virtual void set_cancel(bool f) {
-            std::cout << "set cancel\n";
             m_solver->set_cancel(f);
             m_pb2bv.set_cancel(f);
             #pragma omp critical (sls_solver)
diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp
index 2d7586300..0fe17a29a 100644
--- a/src/opt/pb_sls.cpp
+++ b/src/opt/pb_sls.cpp
@@ -301,6 +301,7 @@ namespace smt {
                 clause const& cls = clauses[i];
                 for (unsigned j = 0; j < cls.m_lits.size(); ++j) {
                     literal lit = cls.m_lits[j];
+                    if (occ.size() <= static_cast<unsigned>(lit.var())) occ.resize(lit.var() + 1);
                     occ[lit.var()].push_back(i);
                 }
             }
@@ -314,6 +315,10 @@ namespace smt {
             m_soft_false.reset();
             m_soft_occ.reset();
             m_penalty.reset();
+            for (unsigned i = 0; i <= m_var2decl.size(); ++i) {
+                m_soft_occ.push_back(unsigned_vector());
+                m_hard_occ.push_back(unsigned_vector());
+            }
 
             // initialize the occurs vectors.
             init_occ(m_clauses, m_hard_occ);
@@ -443,7 +448,6 @@ namespace smt {
         }
 
         int flip(literal l) {
-            SASSERT(get_value(l));
             m_assignment[l.var()] = !m_assignment[l.var()];
             int break_count = 0;
             unsigned_vector const& occh = m_hard_occ[l.var()];
@@ -484,7 +488,6 @@ namespace smt {
                 }
             }                
 
-            SASSERT(get_value(~l));
             TRACE("opt", tout << "flip: " << l << " num false: " << m_hard_false.num_elems() 
                   << " penalty: " << m_penalty << " break count: " << break_count << "\n";);
             return break_count;
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 7087e795d..774147b91 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -162,7 +162,6 @@ namespace opt {
         
         void enable_sls() {
             if (m_enable_sls && probe_bv()) {
-                std::cout << "SLS enabled\n";
                 m_params.set_uint("restarts", 20);
                 m_s = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params);
             }