merge

.gitignore

@@ -65,3 +65,5 @@ src/api/java/Native.cpp
 src/api/java/Native.java
 src/api/java/enumerations/*.java
 *.bak
+doc/api
+doc/code

RELEASE_NOTES

@@ -1,5 +1,10 @@
 RELEASE NOTES
 
+Version 4.3.3
+=============
+
+- Fixed bug in floating point models
+
 Version 4.3.2
 =============
 

doc/website.dox

@@ -15,5 +15,5 @@
    - <a class="el" href="class_microsoft_1_1_z3_1_1_context.html">.NET API</a>
    - <a class="el" href="namespacecom_1_1microsoft_1_1z3.html">Java API</a>
    - <a class="el" href="namespacez3py.html">Python API</a> (also available in <a class="el" href="z3.html">pydoc format</a>).
-   - Try Z3 online at <a href="http://rise4fun.com/z3py">RiSE4Fun</a> using <a href="http://rise4fun.com/z3py">Python</a> or <a href="http://rise4fun.com/z3">SMT 2.0</a>.
+   - Try Z3 online at <a href="http://rise4fun.com/z3">RiSE4Fun</a>.
 */

examples/c++/example.cpp

@@ -21,6 +21,7 @@ void demorgan() {
     // adding the negation of the conjecture as a constraint.
     s.add(!conjecture);
     std::cout << s << "\n";
+    std::cout << s.to_smt2() << "\n";
     switch (s.check()) {
     case unsat:   std::cout << "de-Morgan is valid\n"; break;
     case sat:     std::cout << "de-Morgan is not valid\n"; break;

scripts/mk_project.py

@@ -9,7 +9,7 @@ from mk_util import *
 
 # Z3 Project definition
 def init_project_def():
-    set_version(4, 3, 2, 0)
+    set_version(4, 3, 3, 0)
     add_lib('util', [])
     add_lib('polynomial', ['util'], 'math/polynomial')
     add_lib('sat', ['util'])

src/api/c++/z3++.h

@@ -1314,6 +1314,26 @@ namespace z3 {
         expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
         expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
         friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
+
+        std::string to_smt2(char const* status = "unknown") {
+            array<Z3_ast> es(assertions());
+            Z3_ast const* fmls = es.ptr();
+            Z3_ast fml = 0;
+            unsigned sz = es.size();
+            if (sz > 0) {
+                --sz;
+                fml = fmls[sz];
+            }
+            else {
+                fml = ctx().bool_val(true);
+            }
+            return std::string(Z3_benchmark_to_smtlib_string(
+                                   ctx(),
+                                   "", "", status, "", 
+                                   sz, 
+                                   fmls, 
+                                   fml));
+        }
     };
 
     class goal : public object {

src/api/dotnet/Microsoft.Z3.csproj

@@ -19,12 +19,12 @@
     <DebugSymbols>true</DebugSymbols>
     <DebugType>full</DebugType>
     <Optimize>false</Optimize>
-    <OutputPath>..\..\..\..\..\cwinter\bugs\z3bugs\Debug\</OutputPath>
+    <OutputPath>..\Debug\</OutputPath>
     <DefineConstants>DEBUG;TRACE</DefineConstants>
     <ErrorReport>prompt</ErrorReport>
     <WarningLevel>4</WarningLevel>
     <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>C:\cwinter\bugs\z3bugs\Debug\Microsoft.Z3.XML</DocumentationFile>
+    <DocumentationFile>..\Debug\Microsoft.Z3.XML</DocumentationFile>
     <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
     <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
     <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
@@ -254,7 +254,7 @@
   </PropertyGroup>
   <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">
     <DebugSymbols>true</DebugSymbols>
-    <OutputPath>..\..\..\..\..\cwinter\bugs\z3bugs\Debug\</OutputPath>
+    <OutputPath>..\x86\Debug\</OutputPath>
     <DefineConstants>DEBUG;TRACE</DefineConstants>
     <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
     <DebugType>full</DebugType>
@@ -266,7 +266,7 @@
     <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
     <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
     <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
-    <DocumentationFile>C:\cwinter\bugs\z3bugs\Debug\Microsoft.Z3.XML</DocumentationFile>
+    <DocumentationFile>..\x86\Debug\Microsoft.Z3.XML</DocumentationFile>
   </PropertyGroup>
   <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">
     <OutputPath>bin\x86\Release\</OutputPath>

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):
@@ -453,7 +453,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):
@@ -595,7 +595,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
@@ -743,7 +743,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`.
@@ -1540,7 +1540,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.
@@ -1605,7 +1605,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."""
@@ -6033,20 +6033,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)
 
 
 
@@ -6166,7 +6166,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),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):
@@ -6194,7 +6194,7 @@ class Fixedpoint(Z3PPObject):
             if sz == 1:
                 query = query[0]
             else:
-                query = And(query)
+                query = And(query, self.ctx)
             query = self.abstract(query, False)
             r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
         return CheckSatResult(r)
@@ -6213,7 +6213,7 @@ class Fixedpoint(Z3PPObject):
             name = ""
         name = to_symbol(name, self.ctx)
         body = _get_args(body)
-        f    = self.abstract(Implies(And(body),head))
+        f    = self.abstract(Implies(And(body, self.ctx),head))
         Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
 
     def get_answer(self):       

src/api/z3_api.h

@@ -3988,6 +3988,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)))
@@ -3996,6 +4002,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

@@ -316,6 +316,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_exit_on_error(false),
     m_manager(m),   
     m_own_manager(m == 0),
+    m_manager_initialized(false),
     m_pmanager(0),
     m_sexpr_manager(0),
     m_regular("stdout", std::cout),
@@ -326,8 +327,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());
     }
@@ -471,6 +470,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" ||
@@ -587,17 +596,26 @@ 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());
     }
     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) {
@@ -620,12 +638,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() {
@@ -1165,12 +1193,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) {
@@ -1211,8 +1242,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();
@@ -1332,8 +1362,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();
     if (m_solver) {
         m_check_sat_result = m_solver.get(); // solver itself stores the result.
         m_solver->set_progress_callback(this);

src/cmd_context/cmd_context.h

@@ -149,6 +149,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;
@@ -213,6 +214,7 @@ protected:
     void register_builtin_sorts(decl_plugin * p);
     void register_builtin_ops(decl_plugin * p);
     void register_plugin(symbol const & name, decl_plugin * p, bool install_names);
+    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();
@@ -293,7 +295,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/interp/iz3base.h

@@ -161,7 +161,7 @@ class iz3base : public iz3mgr, public scopes {
   stl_ext::hash_map<ast,ast> simplify_memo;
   stl_ext::hash_map<ast,int> frame_map;                      // map assertions to frames
 
-  int frames;                               // number of frames
+  // int frames;                               // number of frames
 
  protected:
   void add_frame_range(int frame, ast t);

src/interp/iz3proof_itp.cpp

@@ -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/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);

src/tactic/fpa/fpa2bv_model_converter.cpp

@@ -112,13 +112,24 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         unsigned sbits = fu.get_sbits(var->get_range());
 
         expr_ref sgn(m), sig(m), exp(m);        
-        sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl());
+        bv_mdl->eval(a->get_arg(0), sgn, true);
-        sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
+        bv_mdl->eval(a->get_arg(1), sig, true);
-        exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
+        bv_mdl->eval(a->get_arg(2), exp, true);
 
+        SASSERT(a->is_app_of(fu.get_family_id(), OP_TO_FLOAT));
+
+#ifdef Z3DEBUG                
+        SASSERT(to_app(a->get_arg(0))->get_decl()->get_arity() == 0);
+        SASSERT(to_app(a->get_arg(1))->get_decl()->get_arity() == 0);
+        SASSERT(to_app(a->get_arg(1))->get_decl()->get_arity() == 0);        
         seen.insert(to_app(a->get_arg(0))->get_decl());
         seen.insert(to_app(a->get_arg(1))->get_decl());
         seen.insert(to_app(a->get_arg(2))->get_decl());
+#else        
+        SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT);
+        SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT);
+        seen.insert(to_app(to_app(a->get_arg(0))->get_arg(0))->get_decl());
+#endif
 
         if (!sgn && !sig && !exp)
             continue;