Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/api/api_context.cpp

@@ -128,6 +128,7 @@ namespace api {
             for (unsigned i = 0; i < m_replay_stack.size(); ++i) {
                 dealloc(m_replay_stack[i]);
             }
+            m_ast_trail.reset();
         }
         reset_parser();
         dealloc(m_solver);
@@ -360,6 +361,7 @@ namespace api {
                 }
             }
         }
+        SASSERT(num_scopes <= get_smt_kernel().get_scope_level());
         get_smt_kernel().pop(num_scopes);
     }
 

src/api/api_interp.cpp

@@ -411,7 +411,7 @@ static void get_file_params(const char *filename, hash_map<std::string,std::stri
       for(unsigned i = 0; i < tokens.size(); i++){
 	std::string &tok = tokens[i];
 	size_t eqpos = tok.find('=');
-	if(eqpos >= 0 && eqpos < tok.size()){
+	if(eqpos != std::string::npos){
 	  std::string left = tok.substr(0,eqpos);
 	  std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1);
 	  params[left] = right;

src/api/api_solver_old.cpp

@@ -40,7 +40,7 @@ extern "C" {
         LOG_Z3_pop(c, num_scopes);
         RESET_ERROR_CODE();
         CHECK_SEARCHING(c);
-        if (num_scopes > mk_c(c)->get_smt_kernel().get_scope_level()) {
+        if (num_scopes > mk_c(c)->get_num_scopes()) {
             SET_ERROR_CODE(Z3_IOB);
             return;
         }

src/api/python/z3.py

@@ -6960,7 +6960,7 @@ def substitute(t, *m):
     if isinstance(m, tuple):
         m1 = _get_args(m)
         if isinstance(m1, list):
-            m = _get_args(m1)
+            m = m1
     if __debug__:
         _z3_assert(is_expr(t), "Z3 expression expected")
         _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")

src/api/z3_api.h

@@ -7069,7 +7069,7 @@ END_MLAPI_EXCLUDE
        \mlonly then a valid model is returned.  Otherwise, it is unsafe to use the returned model.\endmlonly
        \conly The caller is responsible for deleting the model using the function #Z3_del_model.
        
-       \conly \remark In constrast with the rest of the Z3 API, the reference counter of the
+       \conly \remark In contrast with the rest of the Z3 API, the reference counter of the
        \conly model is incremented. This is to guarantee backward compatibility. In previous
        \conly versions, models did not support reference counting.
        
@@ -7182,6 +7182,11 @@ END_MLAPI_EXCLUDE
        \brief Delete a model object.
        
        \sa Z3_check_and_get_model
+
+       \conly \remark The Z3_check_and_get_model automatically increments a reference count on the model.
+       \conly The expected usage is that models created by that method are deleted using Z3_del_model.
+       \conly This is for backwards compatibility and in contrast to the rest of the API where
+       \conly callers are responsible for managing reference counts.
     
        \deprecated Subsumed by Z3_solver API
        

src/smt/smt_model_checker.cpp

@@ -136,9 +136,8 @@ namespace smt {
         if (cex == 0)
             return false; // no model available.
         unsigned num_decls = q->get_num_decls();
-        unsigned   num_sks = sks.size();
         // Remark: sks were created for the flat version of q.
-        SASSERT(num_sks >= num_decls); 
+        SASSERT(sks.size() >= num_decls);
         expr_ref_buffer bindings(m_manager);
         bindings.resize(num_decls);
         unsigned max_generation = 0;