Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

src/api/python/z3util.py

@@ -210,18 +210,18 @@ def prove(claim,assume=None,verbose=0):
 
 
     if verbose >= 2:
-        print 'assume: '
-        print assume
-        print 'claim: '
-        print claim
-        print 'to_prove: '
-        print to_prove
+        print('assume: ')
+        print(assume)
+        print('claim: ')
+        print(claim)
+        print('to_prove: ')
+        print(to_prove)
 
     f = Not(to_prove)
 
     models = get_models(f,k=1)
     if models is None: #unknown
-        print 'E: cannot solve !'
+        print('E: cannot solve !')
         return None, None
     elif models == False: #unsat
         return True,None   
@@ -458,7 +458,7 @@ def model_str(m,as_str=True):
 
     if m :
         vs = [(v,m[v]) for v in m]
-        vs = sorted(vs,key=lambda (a,_): str(a)) 
+        vs = sorted(vs,key=lambda a,_: str(a))
         if as_str:
             return '\n'.join(['{} = {}'.format(k,v) for (k,v) in vs])
         else:

src/api/z3_api.h

@@ -594,7 +594,10 @@ typedef enum
           }
           This proof object has one antecedent: a hypothetical proof for false.
           It converts the proof in a proof for (or (not l_1) ... (not l_n)),
-          when T1 contains the hypotheses: l_1, ..., l_n.
+          when T1 contains the open hypotheses: l_1, ..., l_n.
+          The hypotheses are closed after an application of a lemma.
+          Furthermore, there are no other open hypotheses in the subtree covered by
+          the lemma.
 
    - Z3_OP_PR_UNIT_RESOLUTION: 
        \nicebox{

src/smt/theory_wmaxsat.cpp

@@ -55,9 +55,8 @@ void theory_wmaxsat::get_assignment(svector<bool>& result) {
     }
     else {
         std::sort(m_cost_save.begin(), m_cost_save.end());
-        unsigned j = 0;
-        for (theory_var i = 0; i < m_vars.size(); ++i) {
-            if (j < m_cost_save.size() && m_cost_save[j] == i) {
+        for (unsigned i = 0,j = 0; i < m_vars.size(); ++i) {
+            if (j < m_cost_save.size() && m_cost_save[j] == static_cast<theory_var>(i)) {
                 result.push_back(false);
                 ++j;
             }

src/test/pdr.cpp

@@ -47,10 +47,15 @@ struct test_model_search {
     void add_tree(model_node* parent, bool force_goal) {
         unsigned level = parent->level();
         search.add_leaf(*parent);
+        expr_ref state(m);
         if (level > 0 && (force_goal || parent->is_goal())) {
             search.remove_goal(*parent);
-            add_tree(alloc(model_node, parent, mk_state(states, rand), pt, level-1), false);
-            add_tree(alloc(model_node, parent, mk_state(states, rand), pt, level-1), false);
+
+            state = mk_state(states, rand);
+            add_tree(alloc(model_node, parent, state, pt, level-1), false);
+
+            state = mk_state(states, rand);
+            add_tree(alloc(model_node, parent, state, pt, level-1), false);
             parent->check_pre_closed();
         }
     }
@@ -91,7 +96,8 @@ struct test_model_search {
         state = states[0].get();
         unsigned level = 4;
         for(unsigned n = 0; n < 100; ++n) {
-            model_node* root = alloc(model_node, 0, mk_state(states, rand), pt, level);
+            state = mk_state(states, rand);
+            model_node* root = alloc(model_node, 0, state, pt, level);
             search.set_root(root);
             add_tree(root, false);
             search.display(std::cout);