local changes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/dotnet/Readme.NET35

@@ -0,0 +1,9 @@
+The default Z3 bindings for .NET are built for the .NET framework version 4.
+Should the need arise, it is also possible to build them for .NET 3.5; the
+instructions are as follows:
+
+In the project properties of Microsoft.Z3.csproj:
+- Under 'Application': Change Target framework to .NET Framework 3.5
+- Under 'Build': Add FRAMEWORK_LT_4 to the condidional compilation symbols
+- Remove the reference to System.Numerics
+- Install the NuGet Package "Microsoft Code Contracts for Net3.5"

src/api/python/z3.py

@@ -298,8 +298,8 @@ class AstRef(Z3PPObject):
         return self.ast
 
     def get_id(self):
-	"""Return unique identifier for object. It can be used for hash-tables and maps."""
+        """Return unique identifier for object. It can be used for hash-tables and maps."""
-	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+        return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
 
     def ctx_ref(self):
         """Return a reference to the C context where this AST node is stored."""
@@ -452,7 +452,7 @@ class SortRef(AstRef):
         return Z3_sort_to_ast(self.ctx_ref(), self.ast)
 
     def get_id(self):
-	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+        return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
 
     def kind(self):
         """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
@@ -593,7 +593,7 @@ class FuncDeclRef(AstRef):
         return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
 
     def get_id(self):
-	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+        return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
 
     def as_func_decl(self):
         return self.ast
@@ -741,7 +741,7 @@ class ExprRef(AstRef):
         return self.ast
 
     def get_id(self):
-	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+        return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
 
     def sort(self):
         """Return the sort of expression `self`.
@@ -1538,7 +1538,7 @@ class PatternRef(ExprRef):
         return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
 
     def get_id(self):
-	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+        return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
 
 def is_pattern(a):
     """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
@@ -1603,7 +1603,7 @@ class QuantifierRef(BoolRef):
         return self.ast
 
     def get_id(self):
-	return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+        return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
 
     def sort(self):
         """Return the Boolean sort."""
@@ -6031,20 +6031,20 @@ 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"""
+        """return SMTLIB2 formatted benchmark for solver's assertions"""
-	es = self.assertions()
+        es = self.assertions()
-	sz = len(es)
+        sz = len(es)
-	sz1 = sz
+        sz1 = sz
-	if sz1 > 0:
+        if sz1 > 0:
-	    sz1 -= 1
+            sz1 -= 1
-	v = (Ast * sz1)()
+        v = (Ast * sz1)()
-	for i in range(sz1):
+        for i in range(sz1):
-	    v[i] = es[i].as_ast()
+            v[i] = es[i].as_ast()
-	if sz > 0:
+        if sz > 0:
-	    e = es[sz1].as_ast()
+            e = es[sz1].as_ast()
-	else:
+        else:
-	    e = BoolVal(True, self.ctx).as_ast()
+            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)
+            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. 
@@ -6162,7 +6162,7 @@ class Fixedpoint(Z3PPObject):
             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)            
         else:
             body = _get_args(body)
-            f    = self.abstract(Implies(And(body,self.ctx),head))
+            f    = self.abstract(Implies(And(body, self.ctx),head))
             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
         
     def rule(self, head, body = None, name = None):

src/api/z3_api.h

@@ -4028,6 +4028,12 @@ END_MLAPI_EXCLUDE
 
     /**
         \brief Return a unique identifier for \c t.
+        The identifier is unique up to structural equality. Thus, two ast nodes
+        created by the same context and having the same children and same function symbols
+        have the same identifiers. Ast nodes created in the same context, but having
+        different children or different functions have different identifiers.
+        Variables and quantifiers are also assigned different identifiers according to
+        their structure.        
         \mlonly \remark Implicitly used by [Pervasives.compare] for values of type [ast], [app], [sort], [func_decl], and [pattern]. \endmlonly
 
         def_API('Z3_get_ast_id', UINT, (_in(CONTEXT), _in(AST)))
@@ -4036,6 +4042,8 @@ END_MLAPI_EXCLUDE
 
     /**
        \brief Return a hash code for the given AST.
+       The hash code is structural. You can use Z3_get_ast_id interchangably with 
+       this function.
        \mlonly \remark Implicitly used by [Hashtbl.hash] for values of type [ast], [app], [sort], [func_decl], and [pattern]. \endmlonly
 
        def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST)))

src/ast/ast.cpp

@@ -1013,6 +1013,17 @@ func_decl * basic_decl_plugin::mk_ite_decl(sort * s) {
     return m_ite_decls[id];
 }
 
+sort* basic_decl_plugin::join(sort* s1, sort* s2) {
+    if (s1 == s2) return s1;
+    if (s1->get_family_id() == m_manager->m_arith_family_id && 
+        s2->get_family_id() == m_manager->m_arith_family_id) {
+        if (s1->get_decl_kind() == REAL_SORT) {
+            return s1;
+        }
+    }
+    return s2;
+}
+
 func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                           unsigned arity, sort * const * domain, sort * range) {
     switch (static_cast<basic_op_kind>(k)) {
@@ -1025,10 +1036,10 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_IFF:     return m_iff_decl;
     case OP_IMPLIES: return m_implies_decl;
     case OP_XOR:     return m_xor_decl;
-    case OP_ITE:     return arity == 3 ? mk_ite_decl(domain[1]) : 0;
+    case OP_ITE:     return arity == 3 ? mk_ite_decl(join(domain[1], domain[2])) : 0;
         // eq and oeq must have at least two arguments, they can have more since they are chainable
-    case OP_EQ:      return arity >= 2 ? mk_eq_decl_core("=", OP_EQ, domain[0], m_eq_decls) : 0;
+    case OP_EQ:      return arity >= 2 ? mk_eq_decl_core("=", OP_EQ, join(domain[0],domain[1]), m_eq_decls) : 0;
-    case OP_OEQ:     return arity >= 2 ? mk_eq_decl_core("~", OP_OEQ, domain[0], m_oeq_decls) : 0;
+    case OP_OEQ:     return arity >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(domain[0],domain[1]), m_oeq_decls) : 0;
     case OP_DISTINCT: {
         func_decl_info info(m_family_id, OP_DISTINCT);
         info.set_pairwise();
@@ -1061,10 +1072,12 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_IFF:     return m_iff_decl;
     case OP_IMPLIES: return m_implies_decl;
     case OP_XOR:     return m_xor_decl;
-    case OP_ITE:     return num_args == 3 ? mk_ite_decl(m_manager->get_sort(args[1])): 0;
+    case OP_ITE:     return num_args == 3 ? mk_ite_decl(join(m_manager->get_sort(args[1]), m_manager->get_sort(args[2]))): 0;
         // eq and oeq must have at least two arguments, they can have more since they are chainable
-    case OP_EQ:      return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, m_manager->get_sort(args[0]), m_eq_decls) : 0;
+    case OP_EQ:      return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, join(m_manager->get_sort(args[0]),
-    case OP_OEQ:     return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, m_manager->get_sort(args[0]), m_oeq_decls) : 0;
+                                                                             m_manager->get_sort(args[1])), m_eq_decls) : 0;
+    case OP_OEQ:     return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(m_manager->get_sort(args[0]),
+                                                                              m_manager->get_sort(args[1])), m_oeq_decls) : 0;
     case OP_DISTINCT:
         return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
     default:

src/ast/ast.h

@@ -1100,6 +1100,7 @@ protected:
     virtual void set_manager(ast_manager * m, family_id id);
     func_decl * mk_eq_decl_core(char const * name, decl_kind k, sort * s, ptr_vector<func_decl> & cache);
     func_decl * mk_ite_decl(sort * s);
+    sort* join(sort* s1, sort* s2);
 public:
     basic_decl_plugin();
     
@@ -1378,7 +1379,7 @@ enum proof_gen_mode {
 // -----------------------------------
 
 class ast_manager {
-protected:
+    friend class basic_decl_plugin;
 protected:
     struct config {
         typedef ast_manager              value_manager;

src/ast/fpa/fpa2bv_converter.cpp

@@ -2155,15 +2155,15 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
     SASSERT(f->get_num_parameters() == 1);
     SASSERT(f->get_parameter(0).is_int());
     
-    unsigned ebits = m_util.get_ebits(f->get_range());
+    //unsigned ebits = m_util.get_ebits(f->get_range());
-    unsigned sbits = m_util.get_sbits(f->get_range());
+    //unsigned sbits = m_util.get_sbits(f->get_range());
-    int width = f->get_parameter(0).get_int();
+    //int width = f->get_parameter(0).get_int();
 
-    expr * rm = args[0];
+    //expr * rm = args[0];
-    expr * x = args[1];
+    //expr * x = args[1];
     
-    expr * sgn, *s, *e;
+    //expr * sgn, *s, *e;
-    split(x, sgn, s, e);
+    //split(x, sgn, s, e);
 
     NOT_IMPLEMENTED_YET();
 }
@@ -2173,15 +2173,15 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
     SASSERT(f->get_num_parameters() == 1);
     SASSERT(f->get_parameter(0).is_int());
 
-    unsigned ebits = m_util.get_ebits(f->get_range());
+    //unsigned ebits = m_util.get_ebits(f->get_range());
-    unsigned sbits = m_util.get_sbits(f->get_range());
+    //unsigned sbits = m_util.get_sbits(f->get_range());
-    int width = f->get_parameter(0).get_int();
+    //int width = f->get_parameter(0).get_int();
 
-    expr * rm = args[0];
+    //expr * rm = args[0];
-    expr * x = args[1];
+    //expr * x = args[1];
 
-    expr * sgn, *s, *e;
+    //expr * sgn, *s, *e;
-    split(x, sgn, s, e);
+    //split(x, sgn, s, e);
 
     NOT_IMPLEMENTED_YET();
 }
@@ -2189,15 +2189,15 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
 void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 1);
 
-    unsigned ebits = m_util.get_ebits(f->get_range());
+    //unsigned ebits = m_util.get_ebits(f->get_range());
-    unsigned sbits = m_util.get_sbits(f->get_range());
+    //unsigned sbits = m_util.get_sbits(f->get_range());
-    int width = f->get_parameter(0).get_int();
+    //int width = f->get_parameter(0).get_int();
 
-    expr * rm = args[0];
+    //expr * rm = args[0];
-    expr * x = args[1];
+    //expr * x = args[1];
 
-    expr * sgn, *s, *e;
+    //expr * sgn, *s, *e;
-    split(x, sgn, s, e);
+    //split(x, sgn, s, e);
 
     NOT_IMPLEMENTED_YET();
 }

src/cmd_context/cmd_context.cpp

@@ -315,8 +315,9 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_numeral_as_real(false),
     m_ignore_check(false),
     m_exit_on_error(false),
-    m_manager(m),
+    m_manager(m),   
     m_own_manager(m == 0),
+    m_manager_initialized(false),
     m_pmanager(0),
     m_sexpr_manager(0),
     m_regular("stdout", std::cout),
@@ -327,8 +328,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     install_core_tactic_cmds(*this);
     install_interpolant_cmds(*this);
     SASSERT(m != 0 || !has_manager());
-    if (m)
-        init_external_manager();
     if (m_main_ctx) { 
         set_verbose_stream(diagnostic_stream());
     }
@@ -484,6 +483,16 @@ void cmd_context::register_plugin(symbol const & name, decl_plugin * p, bool ins
     }
 }
 
+void cmd_context::load_plugin(symbol const & name, bool install, svector<family_id>& fids) {
+    family_id id = m_manager->get_family_id(name);
+    decl_plugin* p = m_manager->get_plugin(id);
+    if (install && p && fids.contains(id)) {
+        register_builtin_sorts(p);
+        register_builtin_ops(p);
+    }
+    fids.erase(id);
+}
+
 bool cmd_context::logic_has_arith_core(symbol const & s) const {
     return 
         s == "QF_LRA" ||
@@ -601,18 +610,27 @@ void cmd_context::init_manager_core(bool new_manager) {
         register_builtin_sorts(basic);
         register_builtin_ops(basic);
         // the manager was created by the command context.
-        register_plugin(symbol("arith"), alloc(arith_decl_plugin), logic_has_arith());
+        register_plugin(symbol("arith"),    alloc(arith_decl_plugin), logic_has_arith());
-        register_plugin(symbol("bv"), alloc(bv_decl_plugin), logic_has_bv());
+        register_plugin(symbol("bv"),       alloc(bv_decl_plugin), logic_has_bv());
-        register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array());
+        register_plugin(symbol("array"),    alloc(array_decl_plugin), logic_has_array());
         register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype());
         register_plugin(symbol("seq"),      alloc(seq_decl_plugin), logic_has_seq());
         register_plugin(symbol("float"),    alloc(float_decl_plugin), logic_has_floats());
         register_plugin(symbol("pb"),     alloc(pb_decl_plugin), !has_logic());
     }
     else {
-        // the manager was created by an external module, we must register all plugins available in the manager.
+        // the manager was created by an external module
+        // we register all plugins available in the manager.
+        // unless the logic specifies otherwise.
         svector<family_id> fids;
         m_manager->get_range(fids);
+        load_plugin(symbol("arith"),    logic_has_arith(), fids);
+        load_plugin(symbol("bv"),       logic_has_bv(), fids);
+        load_plugin(symbol("array"),    logic_has_array(), fids);
+        load_plugin(symbol("datatype"), logic_has_datatype(), fids);
+        load_plugin(symbol("seq"),      logic_has_seq(), fids);
+        load_plugin(symbol("float"),    logic_has_floats(), fids);
+        
         svector<family_id>::iterator it  = fids.begin();
         svector<family_id>::iterator end = fids.end();
         for (; it != end; ++it) {
@@ -635,12 +653,22 @@ void cmd_context::init_manager_core(bool new_manager) {
 }
 
 void cmd_context::init_manager() {
-    SASSERT(m_manager == 0);
+    if (m_manager_initialized) {
-    SASSERT(m_pmanager == 0);
+        // no-op
-    m_check_sat_result = 0;
+    }
-    m_manager  = m_params.mk_ast_manager();
+    else if (m_manager) {
-    m_pmanager = alloc(pdecl_manager, *m_manager);
+        m_manager_initialized = true;
-    init_manager_core(true);
+        SASSERT(!m_own_manager);
+        init_external_manager();
+    }
+    else {
+        m_manager_initialized = true;
+        SASSERT(m_pmanager == 0);
+        m_check_sat_result = 0;
+        m_manager  = m_params.mk_ast_manager();
+        m_pmanager = alloc(pdecl_manager, *m_manager);
+        init_manager_core(true);
+    }
 }
 
 void cmd_context::init_external_manager() {
@@ -1180,12 +1208,15 @@ void cmd_context::reset(bool finalize) {
         if (m_own_manager) {
             dealloc(m_manager);
             m_manager = 0;
+            m_manager_initialized = false;
         }
         else {
             // doesn't own manager... so it cannot be deleted
             // reinit cmd_context if this is not a finalization step
             if (!finalize)
                 init_external_manager();
+            else 
+                m_manager_initialized = false;
         }
     }
     if (m_sexpr_manager) {
@@ -1226,8 +1257,7 @@ void cmd_context::assert_expr(symbol const & name, expr * t) {
 
 void cmd_context::push() {
     m_check_sat_result = 0;
-    if (!has_manager())
+    init_manager();
-        init_manager();
     m_scopes.push_back(scope());
     scope & s = m_scopes.back();
     s.m_func_decls_stack_lim   = m_func_decls_stack.size();
@@ -1351,8 +1381,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         return;
     IF_VERBOSE(100, verbose_stream() << "(started \"check-sat\")" << std::endl;);
     TRACE("before_check_sat", dump_assertions(tout););
-    if (!has_manager())
+    init_manager();
-        init_manager();
     unsigned timeout = m_params.m_timeout;
     scoped_watch sw(*this);
     lbool r;

src/cmd_context/cmd_context.h

@@ -164,6 +164,7 @@ protected:
 
     ast_manager *                m_manager;
     bool                         m_own_manager;
+    bool                         m_manager_initialized;
     pdecl_manager *              m_pmanager;
     sexpr_manager *              m_sexpr_manager;
     check_logic                  m_check_logic;
@@ -228,6 +229,7 @@ protected:
 
     void register_builtin_sorts(decl_plugin * p);
     void register_builtin_ops(decl_plugin * p);
+    void load_plugin(symbol const & name, bool install_names, svector<family_id>& fids);
     void init_manager_core(bool new_manager);
     void init_manager();
     void init_external_manager();
@@ -310,7 +312,7 @@ public:
     std::string reason_unknown() const;
 
     bool has_manager() const { return m_manager != 0; }
-    ast_manager & m() const { if (!m_manager) const_cast<cmd_context*>(this)->init_manager(); return *m_manager; }
+    ast_manager & m() const { const_cast<cmd_context*>(this)->init_manager(); return *m_manager; }
     virtual ast_manager & get_ast_manager() { return m(); }
     pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
     sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }

src/duality/duality.h

@@ -778,6 +778,10 @@ protected:
       struct Bad {
       };
       
+      // thrown on more serious internal error
+      struct ReallyBad {
+      };
+
       /** Pop a scope (see Push). Note, you cannot pop axioms. */
       
       void Pop(int num_scopes);

src/duality/duality_rpfp.cpp

@@ -2643,6 +2643,10 @@ namespace Duality {
 	GetGroundLitsUnderQuants(memo,f.body(),res,1);
       return;
     }
+    if(f.is_var()){
+      //      std::cout << "foo!\n";
+      return;
+    }
     if(under && f.is_ground())
       res.push_back(f);
   }
@@ -3065,10 +3069,14 @@ namespace Duality {
     node->Annotation.SetEmpty();
     hash_set<ast> *core = new hash_set<ast>;
     core->insert(node->Outgoing->dual);
+    expr prev_annot = ctx.bool_val(false);
+    expr prev_impl = ctx.bool_val(false);
+    int repeated_case_count = 0;
     while(1){
       by_case_counter++;
       is.push();
       expr annot = !GetAnnotation(node);
+      Transformer old_annot = node->Annotation;
       is.add(annot);
       if(is.check() == unsat){
 	is.pop(1);
@@ -3076,56 +3084,70 @@ namespace Duality {
       }
       is.pop(1);
       Push();
-      ConstrainEdgeLocalized(node->Outgoing,is.get_implicant());
+      expr the_impl = is.get_implicant();
+      if(eq(the_impl,prev_impl)){
+	//	std::cout << "got old implicant\n";
+	repeated_case_count++;
+      }
+      prev_impl = the_impl;
+      ConstrainEdgeLocalized(node->Outgoing,the_impl);
       ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this?
-      check_result foo = Check(root);
-      if(foo != unsat){
-	slvr().print("should_be_unsat.smt2");
-	throw "should be unsat";
-      }
-      std::vector<expr> assumps, axioms_to_add;
-      slvr().get_proof().get_assumptions(assumps);
-      for(unsigned i = 0; i < assumps.size(); i++){
-	(*core).insert(assumps[i]);
-	if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
-	  axioms_to_add.push_back(assumps[i]);
-	  axioms_needed.erase(assumps[i]);
-	}
-      }
-      // AddToProofCore(*core);
-      Transformer old_annot = node->Annotation;
-      SolveSingleNode(root,node);
-
-      {
-	expr itp = GetAnnotation(node);
-	dualModel = is.get_model(); // TODO: what does this mean?
-	std::vector<expr> case_lits;
-	itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
-	SetAnnotation(node,itp);
-	node->Annotation.Formula = node->Annotation.Formula.simplify();
-      }
-
-      for(unsigned i = 0; i < axioms_to_add.size(); i++)
-	is.add(axioms_to_add[i]);
       
-#define TEST_BAD
-#ifdef TEST_BAD
       {
-	static int bad_count = 0, num_bads = 1;
+	check_result foo = Check(root);
-	if(bad_count >= num_bads){
+	if(foo != unsat){
-	  bad_count = 0;
-	  num_bads = num_bads * 2;
 	  Pop(1);
 	  is.pop(1);
 	  delete core;
 	  timer_stop("InterpolateByCases");
-	  throw Bad();
+	  throw ReallyBad();
+	  // slvr().print("should_be_unsat.smt2");
+	  // throw "should be unsat";
 	}
-	bad_count++;
+	std::vector<expr> assumps, axioms_to_add;
-      }
+	slvr().get_proof().get_assumptions(assumps);
-#endif
+	for(unsigned i = 0; i < assumps.size(); i++){
+	  (*core).insert(assumps[i]);
+	  if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
+	    axioms_to_add.push_back(assumps[i]);
+	    axioms_needed.erase(assumps[i]);
+	  }
+	}
+	// AddToProofCore(*core);
+	SolveSingleNode(root,node);
 
-      if(node->Annotation.IsEmpty()){
+	{
+	  expr itp = GetAnnotation(node);
+	  dualModel = is.get_model(); // TODO: what does this mean?
+	  std::vector<expr> case_lits;
+	  itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
+	  SetAnnotation(node,itp);
+	  node->Annotation.Formula = node->Annotation.Formula.simplify();
+	}
+
+	for(unsigned i = 0; i < axioms_to_add.size(); i++)
+	  is.add(axioms_to_add[i]);
+      
+#define TEST_BAD
+#ifdef TEST_BAD
+	{
+	  static int bad_count = 0, num_bads = 1;
+	  if(bad_count >= num_bads){
+	    bad_count = 0;
+	    num_bads = num_bads * 2;
+	    Pop(1);
+	    is.pop(1);
+	    delete core;
+	    timer_stop("InterpolateByCases");
+	    throw Bad();
+	  }
+	  bad_count++;
+	}
+#endif
+      }
+
+      if(node->Annotation.IsEmpty() || eq(node->Annotation.Formula,prev_annot) || (repeated_case_count > 0 && !axioms_added) || (repeated_case_count >= 10)){
+      looks_bad:
 	if(!axioms_added){
 	  // add the axioms in the off chance they are useful
 	  const std::vector<expr> &theory = ls->get_axioms();
@@ -3134,6 +3156,7 @@ namespace Duality {
 	  axioms_added = true;
 	}
 	else {
+	  //#define KILL_ON_BAD_INTERPOLANT	  
 #ifdef KILL_ON_BAD_INTERPOLANT	  
 	  std::cout << "bad in InterpolateByCase -- core:\n";
 #if 0
@@ -3175,10 +3198,11 @@ namespace Duality {
 	  is.pop(1);
 	  delete core;
 	  timer_stop("InterpolateByCases");
-	  throw Bad();
+	  throw ReallyBad();
 	}
       }
       Pop(1);
+      prev_annot = node->Annotation.Formula;
       node->Annotation.UnionWith(old_annot);
     }
     if(proof_core)

src/duality/duality_solver.cpp

@@ -2279,6 +2279,18 @@ namespace Duality {
 		  // bad interpolants can get us here
 		  throw DoRestart();
 		}
+		catch(const RPFP::ReallyBad &){
+		  // this could be caused by incompleteness
+		  for(unsigned i = 0; i < expansions.size(); i++){
+		    Node *node = expansions[i];
+		    node->map->Annotation.SetFull();
+		    std::vector<Node *> &chs = node->map->Outgoing->Children;
+		    for(unsigned j = 0; j < chs.size(); j++)
+		      chs[j]->Annotation.SetFull();
+		    reporter->Message("incompleteness: cleared annotation and child annotations");
+		  }
+		  throw DoRestart();
+		}
 		catch(char const *msg){
 		  // bad interpolants can get us here
 		  reporter->Message(std::string("interpolation failure:") + msg);

src/interp/iz3mgr.cpp

@@ -778,6 +778,8 @@ int iz3mgr::occurs_in(ast var, ast e){
 
 
 bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){
+  if(occurs_in(v,y))
+    return false;
   if(op(x) == Plus){
     int n = num_args(x);
     for(int i = 0; i < n; i++){
@@ -801,8 +803,8 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, as
     return ast();
   cont_eq_memo.insert(e);
   if(!truth && op(e) == Equal){
-    if(arg(e,0) == v) return(arg(e,1));
+    if(arg(e,0) == v && !occurs_in(v,arg(e,1))) return(arg(e,1));
-    if(arg(e,1) == v) return(arg(e,0));
+    if(arg(e,1) == v && !occurs_in(v,arg(e,0))) return(arg(e,0));
     ast res;
     if(solve_arith(v,arg(e,0),arg(e,1),res)) return res;
     if(solve_arith(v,arg(e,1),arg(e,0),res)) return res;

src/interp/iz3mgr.h

@@ -278,7 +278,8 @@ class iz3mgr  {
   }
 
   symb sym(ast t){
-    return to_app(t.raw())->get_decl();
+    raw_ast *_ast = t.raw();
+    return is_app(_ast) ? to_app(_ast)->get_decl() : 0;
   }
 
   std::string string_of_symbol(symb s){

src/interp/iz3proof_itp.cpp

@@ -1027,7 +1027,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	linear_comb(Aineqs,coeff,make(Leq,make_int(rational(0)),make(Sub,term2,term1)));
     }
     else {
-      ast pf = extract_rewrites(make(concat,mk_true(),rest),p1);
+      ast pf = extract_rewrites(make(concat,mk_true(),last),p1);
       ast new_normal = fix_normal(term1,term2,pf);
       normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
     }
@@ -2747,7 +2747,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast orig_e = e;
     pf = make_refl(e);  // proof that e = e
 
-    prover::range erng = pv->ast_scope(e);
+    // prover::range erng = 
+    pv->ast_scope(e);
 #if 0
     if(!(erng.lo > erng.hi) && pv->ranges_intersect(pv->ast_scope(e),rng)){
       return e; // this term occurs in range, so it's O.K.

src/interp/iz3translate.cpp

@@ -1712,11 +1712,17 @@ public:
 	std::cout << "foo!\n";
 
       // no idea why this shows up
-      if(dk == PR_MODUS_PONENS_OEQ)
+      if(dk == PR_MODUS_PONENS_OEQ){
 	if(conc(prem(proof,0)) == con){
 	  res = translate_main(prem(proof,0),expect_clause);
 	  return res;
 	}
+	if(expect_clause && op(con) == Or){ // skolemization does this
+	  Iproof::node clause = translate_main(prem(proof,0),true);
+	  res = RewriteClause(clause,prem(proof,1));
+	  return res;
+	}
+      }
       
 #if 0
       if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
@@ -1800,7 +1806,9 @@ public:
 	}
 	break;
       }
-      case PR_MONOTONICITY: {
+      case PR_QUANT_INTRO:
+      case PR_MONOTONICITY:
+	{
 	std::vector<ast> eqs; eqs.resize(args.size());
 	for(unsigned i = 0; i < args.size(); i++)
 	  eqs[i] = conc(prem(proof,i));

src/smt/theory_array_base.cpp

@@ -362,7 +362,6 @@ namespace smt {
          (store A i v) <--- v is used as an value
     */
     bool theory_array_base::is_shared(theory_var v) const {
-        context & ctx  = get_context();
         enode * n      = get_enode(v);
         enode * r      = n->get_root();
         bool is_array  = false;

src/tactic/bv/bv_size_reduction_tactic.cpp

@@ -151,7 +151,7 @@ struct bv_size_reduction_tactic::imp {
                             // bound is infeasible.
                         } 
                         else {
-                            update_signed_upper(to_app(lhs), val);
+                            update_signed_upper(to_app(rhs), val);
                         }                        
                     }
                     else update_signed_lower(to_app(rhs), val);
@@ -229,17 +229,35 @@ struct bv_size_reduction_tactic::imp {
                         else {
                             // l < u
                             if (l.is_neg()) {
-                                unsigned i_nb = (u - l).get_num_bits();
+                                unsigned l_nb = (-l).get_num_bits();
                                 unsigned v_nb = m_util.get_bv_size(v);
-                                if (i_nb < v_nb) {
+
-                                    new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
+                                if (u.is_neg())
-                                    new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
+                                {
+                                    // l <= v <= u <= 0
+                                    unsigned i_nb = l_nb;
+                                    TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= u <= 0 " << " --> " << i_nb << " bits\n";);
+                                    if (i_nb < v_nb) {
+                                        new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
+                                        new_def = m_util.mk_concat(m_util.mk_numeral(numeral(-1), v_nb - i_nb), new_const);
+                                    }
+                                }
+                                else {
+                                    // l <= v <= 0 <= u
+                                    unsigned u_nb = u.get_num_bits();
+                                    unsigned i_nb = ((l_nb > u_nb) ? l_nb : u_nb) + 1;
+                                    TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= 0 <= u " << " --> " << i_nb << " bits\n";);
+                                    if (i_nb < v_nb) {
+                                        new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
+                                        new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
+                                    }
                                 }
                             }
                             else {
                                 // 0 <= l <= v <= u
                                 unsigned u_nb = u.get_num_bits();
                                 unsigned v_nb = m_util.get_bv_size(v);
+                                TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << " --> " << u_nb << " bits\n";);
                                 if (u_nb < v_nb) {
                                     new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
                                     new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);