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

scripts/update_api.py

@@ -420,7 +420,7 @@ def mk_dotnet():
 
 
 NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
-Unwrapped = [ 'Z3_del_context' ]
+Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
 
 def mk_dotnet_wrappers():
     global Type2Str

src/cmd_context/interpolant_cmds.cpp

@@ -33,6 +33,7 @@ Notes:
 #include"iz3checker.h"
 #include"iz3profiling.h"
 #include"interp_params.hpp"
+#include"scoped_proof.h"
 
 static void show_interpolant_and_maybe_check(cmd_context & ctx,
 					     ptr_vector<ast> &cnsts,
@@ -153,7 +154,7 @@ static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, par
   ast_manager &_m = ctx.m();
   // TODO: the following is a HACK to enable proofs in the old smt solver
   // When we stop using that solver, this hack can be removed
-  _m.toggle_proof_mode(PGM_FINE);  
+  scoped_proof_mode spm(_m,PGM_FINE);
   ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
   p.set_bool("proof", true);
   scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());

src/solver/solver_na2as.cpp

@@ -82,7 +82,7 @@ void solver_na2as::pop(unsigned n) {
 }
 
 void solver_na2as::restore_assumptions(unsigned old_sz) {
-    SASSERT(old_sz == 0);
+  //    SASSERT(old_sz == 0);
     for (unsigned i = old_sz; i < m_assumptions.size(); i++) {
         m_manager.dec_ref(m_assumptions[i]);
     }