Merge branch 'master' of https://github.com/z3prover/z3

scripts/update_api.py

@@ -73,7 +73,7 @@ Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctype
 
 # Mapping to .NET types
 Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double',
-                FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr',
+                FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'bool', SYMBOL : 'IntPtr',
                 PRINT_MODE : 'uint', ERROR_CODE : 'uint' }
 
 # Mapping to Java types

src/ackermannization/ackermannize_bv_tactic.cpp

@@ -35,7 +35,7 @@ public:
         fail_if_proof_generation("ackermannize", g);
         TRACE("ackermannize", g->display(tout << "in\n"););
 
-        expr_ref_vector flas(m);
+        ptr_vector<expr> flas;
         const unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
         lackr lackr(m, m_p, m_st, flas, nullptr);

src/ackermannization/ackr_model_converter.cpp

@@ -134,7 +134,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
         info->abstract(arg, aarg);
         expr_ref arg_value(m);
         evaluator(aarg, arg_value);
-        args.push_back(arg_value);
+        args.push_back(std::move(arg_value));
     }
     if (fi->get_entry(args.c_ptr()) == nullptr) {
         TRACE("ackr_model",

src/ackermannization/lackr.cpp

@@ -23,8 +23,8 @@
 #include "ast/for_each_expr.h"
 #include "model/model_smt2_pp.h"
 
-lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas,
+lackr::lackr(ast_manager& m, const params_ref& p, lackr_stats& st,
-    solver * uffree_solver)
+             const ptr_vector<expr>& formulas, solver * uffree_solver)
     : m_m(m)
     , m_p(p)
     , m_formulas(formulas)
@@ -173,11 +173,10 @@ void lackr::abstract() {
     }
     m_info->seal();
     // perform abstraction of the formulas
-    const unsigned sz = m_formulas.size();
+    for (expr * f : m_formulas) {
-    for (unsigned i = 0; i < sz; ++i) {
         expr_ref a(m_m);
-        m_info->abstract(m_formulas.get(i), a);
+        m_info->abstract(f, a);
-        m_abstr.push_back(a);
+        m_abstr.push_back(std::move(a));
     }
 }
 
@@ -249,13 +248,9 @@ lbool lackr::lazy() {
 // Collect all uninterpreted terms, skipping 0-arity.
 //
 bool lackr::collect_terms() {
-    ptr_vector<expr> stack;
+    ptr_vector<expr> stack = m_formulas;
     expr *           curr;
     expr_mark        visited;
-    for(unsigned i = 0; i < m_formulas.size(); ++i) {
-        stack.push_back(m_formulas.get(i));
-        TRACE("lackr", tout << "infla: " <<mk_ismt2_pp(m_formulas.get(i), m_m, 2) <<  "\n";);
-    }
 
     while (!stack.empty()) {
         curr = stack.back();

src/ackermannization/lackr.h

@@ -42,8 +42,8 @@ struct lackr_stats {
 **/
 class lackr {
     public:
-        lackr(ast_manager& m, params_ref p, lackr_stats& st,
+        lackr(ast_manager& m, const params_ref& p, lackr_stats& st,
-            expr_ref_vector& formulas, solver * uffree_solver);
+              const ptr_vector<expr>& formulas, solver * uffree_solver);
         ~lackr();
         void updt_params(params_ref const & _p);
 
@@ -82,7 +82,7 @@ class lackr {
         typedef ackr_helper::app_set       app_set;
         ast_manager&                         m_m;
         params_ref                           m_p;
-        expr_ref_vector                      m_formulas;
+        const ptr_vector<expr>&              m_formulas;
         expr_ref_vector                      m_abstr;
         fun2terms_map                        m_fun2terms;
         ackr_info_ref                        m_info;

src/api/api_arith.cpp

@@ -120,12 +120,8 @@ extern "C" {
     }
 
     Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) {
-        Z3_TRY;
         LOG_Z3_is_algebraic_number(c, a);
-        RESET_ERROR_CODE();
+        return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a));
-        expr * e = to_expr(a);
-        return mk_c(c)->autil().is_irrational_algebraic_numeral(e);
-        Z3_CATCH_RETURN(Z3_FALSE);
     }
 
     Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) {

src/api/api_context.cpp

@@ -218,10 +218,9 @@ namespace api {
             // Corner case bug: n may be in m_last_result, and this is the only reference to n.
             // When, we execute reset() it is deleted
             // To avoid this bug, I bump the reference counter before reseting m_last_result
-            m().inc_ref(n);
+            ast_ref node(n, m());
             m_last_result.reset();
-            m_last_result.push_back(n);
+            m_last_result.push_back(std::move(node));
-            m().dec_ref(n);
         }
         else {
             m_ast_trail.push_back(n);

src/api/dotnet/AST.cs

@@ -43,7 +43,7 @@ namespace Microsoft.Z3
                    (!Object.ReferenceEquals(a, null) &&
                     !Object.ReferenceEquals(b, null) &&
                     a.Context.nCtx == b.Context.nCtx &&
-                    Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
+                    Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject));
         }
 
         /// <summary>

src/api/dotnet/ASTMap.cs

@@ -37,7 +37,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(k != null);
 
-            return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject) != 0;
+            return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject);
         }
 
         /// <summary>

src/api/dotnet/BitVecNum.cs

@@ -39,7 +39,7 @@ namespace Microsoft.Z3
             get
             {
                 UInt64 res = 0;
-                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a 64 bit unsigned");
                 return res;
             }
@@ -53,7 +53,7 @@ namespace Microsoft.Z3
             get
             {
                 int res = 0;
-                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int");
                 return res;
             }
@@ -67,7 +67,7 @@ namespace Microsoft.Z3
             get
             {
                 Int64 res = 0;
-                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int64");
                 return res;
             }
@@ -81,7 +81,7 @@ namespace Microsoft.Z3
             get
             {
                 uint res = 0;
-                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a uint");
                 return res;
             }

src/api/dotnet/Context.cs

@@ -1963,7 +1963,7 @@ namespace Microsoft.Z3
             Contract.Ensures(Contract.Result<IntExpr>() != null);
 
             CheckContextMatch(t);
-            return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0));
+            return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed)));
         }
 
         /// <summary>
@@ -1980,7 +1980,7 @@ namespace Microsoft.Z3
 
             CheckContextMatch(t1);
             CheckContextMatch(t2);
-            return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
+            return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned)));
         }
 
         /// <summary>
@@ -2031,7 +2031,7 @@ namespace Microsoft.Z3
 
             CheckContextMatch(t1);
             CheckContextMatch(t2);
-            return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
+            return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned)));
         }
 
         /// <summary>
@@ -2080,7 +2080,7 @@ namespace Microsoft.Z3
 
             CheckContextMatch(t1);
             CheckContextMatch(t2);
-            return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0));
+            return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned)));
         }
 
         /// <summary>
@@ -3135,9 +3135,7 @@ namespace Microsoft.Z3
         public BitVecNum MkBV(bool[] bits)
         {
             Contract.Ensures(Contract.Result<BitVecNum>() != null);
-            int[] _bits = new int[bits.Length];
+            return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, bits));
-            for (int i = 0; i < bits.Length; ++i) _bits[i] = bits[i] ? 1 : 0;	
-            return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits));
         }
 
 
@@ -4186,7 +4184,7 @@ namespace Microsoft.Z3
         public FPNum MkFPInf(FPSort s, bool negative)
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0));
+            return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative));
         }
 
         /// <summary>
@@ -4197,7 +4195,7 @@ namespace Microsoft.Z3
         public FPNum MkFPZero(FPSort s, bool negative)
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
+            return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative));
         }
 
         /// <summary>
@@ -4243,7 +4241,7 @@ namespace Microsoft.Z3
         public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn, exp, sig, s.NativeObject));
         }
 
         /// <summary>
@@ -4256,7 +4254,7 @@ namespace Microsoft.Z3
         public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s)
         {
             Contract.Ensures(Contract.Result<FPRMExpr>() != null);
-            return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject));
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn, exp, sig, s.NativeObject));
         }
 
         /// <summary>

src/api/dotnet/Expr.cs

@@ -179,7 +179,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsNumeral
         {
-            get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) ; }
         }
 
         /// <summary>
@@ -188,7 +188,7 @@ namespace Microsoft.Z3
         /// <returns>True if the term is well-sorted, false otherwise.</returns>
         public bool IsWellSorted
         {
-            get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) ; }
         }
 
         /// <summary>
@@ -239,7 +239,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsAlgebraicNumber
         {
-            get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); }
         }
         #endregion
 
@@ -256,7 +256,7 @@ namespace Microsoft.Z3
                 return (IsExpr &&
                         Native.Z3_is_eq_sort(Context.nCtx,
                                               Native.Z3_mk_bool_sort(Context.nCtx),
-                                              Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0);
+                                              Native.Z3_get_sort(Context.nCtx, NativeObject)) );
             }
         }
 
@@ -423,7 +423,7 @@ namespace Microsoft.Z3
         {
             get
             {
-                return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
+                return (Native.Z3_is_app(Context.nCtx, NativeObject)  &&
                         (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
                         == Z3_sort_kind.Z3_ARRAY_SORT);
             }
@@ -789,7 +789,7 @@ namespace Microsoft.Z3
         /// Check whether expression is a string constant.
         /// </summary>
         /// <returns>a Boolean</returns>
-        public bool IsString  { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } }
+        public bool IsString  { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject); } }
 
         /// <summary>
         /// Retrieve string corresponding to string constant.
@@ -1336,7 +1336,7 @@ namespace Microsoft.Z3
         {
             get
             {
-                return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
+                return (Native.Z3_is_app(Context.nCtx, NativeObject)  &&
                         Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
                         == (uint)Z3_sort_kind.Z3_RELATION_SORT);
             }
@@ -1458,7 +1458,7 @@ namespace Microsoft.Z3
         {
             get
             {
-                return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
+                return (Native.Z3_is_app(Context.nCtx, NativeObject)  &&
                         Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
             }
         }
@@ -1789,7 +1789,7 @@ namespace Microsoft.Z3
         [Pure]
         internal override void CheckNativeObject(IntPtr obj)
         {
-            if (Native.Z3_is_app(Context.nCtx, obj) == 0 &&
+            if (Native.Z3_is_app(Context.nCtx, obj) == false &&
                 Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_VAR_AST &&
                 Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_QUANTIFIER_AST)
                 throw new Z3Exception("Underlying object is not a term");
@@ -1822,11 +1822,13 @@ namespace Microsoft.Z3
             IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
             Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s);
 
-            if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0) // is this a numeral ast?
+            if (Z3_sort_kind.Z3_REAL_SORT == sk && 
+                Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast?
                 return new AlgebraicNum(ctx, obj);
 
-            if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
+            if (Native.Z3_is_numeral_ast(ctx.nCtx, obj))
             {
+
                 switch (sk)
                 {
                     case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);

src/api/dotnet/FPNum.cs

@@ -52,7 +52,7 @@ namespace Microsoft.Z3
             get
             {
                 int res = 0;
-                if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Sign is not a Boolean value");
                 return res != 0;
             }
@@ -86,7 +86,7 @@ namespace Microsoft.Z3
             get
             {
                 UInt64 result = 0;
-                if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
+                if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == false)
                     throw new Z3Exception("Significand is not a 64 bit unsigned integer");
                 return result;
             }
@@ -111,7 +111,7 @@ namespace Microsoft.Z3
         /// </summary>
         public string Exponent(bool biased = true)
         {
-            return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased ? 1 : 0);
+            return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased);
         }
 
         /// <summary>
@@ -120,7 +120,7 @@ namespace Microsoft.Z3
         public Int64 ExponentInt64(bool biased = true)
         {
             Int64 result = 0;
-            if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased ? 1 : 0) == 0)
+            if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased) == false)
                 throw new Z3Exception("Exponent is not a 64 bit integer");
             return result;
         }
@@ -133,43 +133,43 @@ namespace Microsoft.Z3
         /// </remarks>
         public BitVecExpr ExponentBV(bool biased = true)
         {
-            return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0));
+            return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased));
         }
 
         /// <summary>
         /// Indicates whether the numeral is a NaN.
         /// </summary>
-        public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } }
+        public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is a +oo or -oo.
         /// </summary>
-        public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } }
+        public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is +zero or -zero.
         /// </summary>
-        public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } }
+        public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is normal.
         /// </summary>
-        public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } }
+        public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is subnormal.
         /// </summary>
-        public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } }
+        public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is positive.
         /// </summary>
-        public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } }
+        public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) ; } }
 
         /// <summary>
         /// Indicates whether the numeral is negative.
         /// </summary>
-        public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } }
+        public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) ; } }
 
         #region Internal
         internal FPNum(Context ctx, IntPtr obj)

src/api/dotnet/FiniteDomainNum.cs

@@ -39,7 +39,7 @@ namespace Microsoft.Z3
             get
             {
                 UInt64 res = 0;
-                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a 64 bit unsigned");
                 return res;
             }
@@ -53,7 +53,7 @@ namespace Microsoft.Z3
             get
             {
                 int res = 0;
-                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int");
                 return res;
             }
@@ -67,7 +67,7 @@ namespace Microsoft.Z3
             get
             {
                 Int64 res = 0;
-                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int64");
                 return res;
             }
@@ -81,7 +81,7 @@ namespace Microsoft.Z3
             get
             {
                 uint res = 0;
-                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a uint");
                 return res;
             }

src/api/dotnet/FuncDecl.cs

@@ -38,7 +38,7 @@ namespace Microsoft.Z3
                    (!Object.ReferenceEquals(a, null) &&
                     !Object.ReferenceEquals(b, null) &&
                     a.Context.nCtx == b.Context.nCtx &&
-                    Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
+                    Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject));
         }
 
         /// <summary>

src/api/dotnet/Global.cs

@@ -65,7 +65,7 @@ namespace Microsoft.Z3
         public static string GetParameter(string id)
         {
             IntPtr t;
-            if (Native.Z3_global_param_get(id, out t) == 0)
+            if (Native.Z3_global_param_get(id, out t) == false)
                 return null;
             else
                 return Marshal.PtrToStringAnsi(t);
@@ -91,7 +91,7 @@ namespace Microsoft.Z3
         /// all contexts globally.</remarks>
         public static void ToggleWarningMessages(bool enabled)
         {
-            Native.Z3_toggle_warning_messages((enabled) ? 1 : 0);
+            Native.Z3_toggle_warning_messages(enabled);
         }
 
         /// <summary>

src/api/dotnet/Goal.cs

@@ -103,7 +103,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool Inconsistent
         {
-            get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) ; }
         }
 
         /// <summary>
@@ -163,7 +163,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsDecidedSat
         {
-            get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) ; }
         }
 
         /// <summary>
@@ -171,7 +171,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsDecidedUnsat
         {
-            get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) ; }
         }
 
 	/// <summary>
@@ -251,7 +251,7 @@ namespace Microsoft.Z3
         internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
         internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
-            : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
+            : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models), (unsatCores), (proofs)))
         {
             Contract.Requires(ctx != null);
         }

src/api/dotnet/IntNum.cs

@@ -49,7 +49,7 @@ namespace Microsoft.Z3
             get
             {
                 UInt64 res = 0;
-                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a 64 bit unsigned");
                 return res;
             }
@@ -63,7 +63,7 @@ namespace Microsoft.Z3
             get
             {
                 int res = 0;
-                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int");
                 return res;
             }
@@ -77,7 +77,7 @@ namespace Microsoft.Z3
             get
             {
                 Int64 res = 0;
-                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not an int64");
                 return res;
             }
@@ -91,7 +91,7 @@ namespace Microsoft.Z3
             get
             {
                 uint res = 0;
-                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
+                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false)
                     throw new Z3Exception("Numeral is not a uint");
                 return res;
             }

src/api/dotnet/Model.cs

@@ -86,7 +86,7 @@ namespace Microsoft.Z3
                         return null;
                     else
                     {
-                        if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
+                        if (Native.Z3_is_as_array(Context.nCtx, n) == false)
                             throw new Z3Exception("Argument was not an array constant");
                         IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
                         return FuncInterp(new FuncDecl(Context, fd));
@@ -227,7 +227,7 @@ namespace Microsoft.Z3
             Contract.Ensures(Contract.Result<Expr>() != null);
 
             IntPtr v = IntPtr.Zero;
-            if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0)
+            if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion), ref v) == false)
                 throw new ModelEvaluationFailedException();
             else
                 return Expr.Create(Context, v);

src/api/dotnet/Params.cs

@@ -35,7 +35,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(name != null);
 
-            Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0);
+            Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value));
             return this;
         }
 
@@ -90,7 +90,7 @@ namespace Microsoft.Z3
         /// </summary>
         public Params Add(string name, bool value)
         {
-            Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
+            Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value));
 	    return this;
         }
 

src/api/dotnet/Quantifier.cs

@@ -33,7 +33,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsUniversal
         {
-            get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); }
         }
 
         /// <summary>
@@ -41,7 +41,7 @@ namespace Microsoft.Z3
         /// </summary>
         public bool IsExistential
         {
-            get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject) != 0; }
+            get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); }
         }
 
         /// <summary>
@@ -193,7 +193,7 @@ namespace Microsoft.Z3
 
             if (noPatterns == null && quantifierID == null && skolemID == null)
             {
-                NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) , weight,
                                            AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
                                            AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
                                            Symbol.ArrayToNative(names),
@@ -201,7 +201,7 @@ namespace Microsoft.Z3
             }
             else
             {
-                NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall), weight,
                                   AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
                                   AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
                                   AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns),
@@ -229,14 +229,14 @@ namespace Microsoft.Z3
 
             if (noPatterns == null && quantifierID == null && skolemID == null)
             {
-                NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) , weight,
                                                  AST.ArrayLength(bound), AST.ArrayToNative(bound),
                                                  AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
                                                  body.NativeObject);
             }
             else
             {
-                NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall) ? 1 : 0, weight,
+                NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall), weight,
                                         AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID),
                                         AST.ArrayLength(bound), AST.ArrayToNative(bound),
                                         AST.ArrayLength(patterns), AST.ArrayToNative(patterns),

src/api/dotnet/Sort.cs

@@ -41,7 +41,7 @@ namespace Microsoft.Z3
                    (!Object.ReferenceEquals(a, null) &&
                     !Object.ReferenceEquals(b, null) &&
                     a.Context == b.Context &&
-                    Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
+                    Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject));
         }
 
         /// <summary>

src/api/dotnet/Statistics.cs

@@ -134,9 +134,9 @@ namespace Microsoft.Z3
                 {
                     Entry e;
                     string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
-                    if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0)
+                    if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) )
                         e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i));
-                    else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0)
+                    else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) )
                         e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i));
                     else
                         throw new Z3Exception("Unknown data entry value");

src/api/z3_logger.h

@@ -49,7 +49,7 @@ void __declspec(noinline) _Z3_append_log(char const * msg) { *g_z3_log << "M \""
 static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) {
     char const * s = d.m_str;
     while (*s) {
-        char c = *s;
+        unsigned char c = *s;
         if (('0' <= c && c <= '9') || ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z') ||
             c == '~' || c == '!' || c == '@' || c == '#' || c == '$' || c == '%' || c == '^' || c == '&' ||
             c == '*' || c == '-' || c == '_' || c == '+' || c == '.' || c == '?' || c == '/' || c == ' ' ||
@@ -57,7 +57,7 @@ static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) {
             out << c;
         }
         else {
-            char str[4] = {'0', '0', '0', 0};
+            unsigned char str[4] = {'0', '0', '0', 0};
             str[2] = '0' + (c % 10);
             c /= 10;
             str[1] = '0' + (c % 10);

src/ast/arith_decl_plugin.cpp

@@ -638,6 +638,11 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int
     return true;
 }
 
+bool arith_recognizers::is_irrational_algebraic_numeral(expr const * n) const { 
+    return is_app(n) && to_app(n)->is_app_of(m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); 
+}
+
+
 #define IS_INT_EXPR_DEPTH_LIMIT 100
 bool arith_recognizers::is_int_expr(expr const *e) const {
     if (is_int(e)) return true;
@@ -678,7 +683,7 @@ void arith_util::init_plugin() {
     m_plugin = static_cast<arith_decl_plugin*>(m_manager.get_plugin(m_afid));
 }
 
-bool arith_util::is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val) {
+bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) {
     if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM))
         return false;
     am().set(val, to_irrational_algebraic_numeral(n));

src/ast/arith_decl_plugin.h

@@ -229,7 +229,7 @@ public:
     family_id get_family_id() const { return m_afid; }
 
     bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == m_afid; }
-    bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
+    bool is_irrational_algebraic_numeral(expr const * n) const;
     bool is_numeral(expr const * n, rational & val, bool & is_int) const;
     bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); }
     bool is_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_NUM); }
@@ -338,8 +338,7 @@ public:
         return plugin().am();
     }
 
-    bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
+    bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val);
-    bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
     algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
 
     sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); }

src/ast/ast_smt2_pp.cpp

@@ -1199,7 +1199,7 @@ void mk_smt2_format(unsigned sz, expr * const* es, smt2_pp_environment & env, pa
     for (unsigned i = 0; i < sz; ++i) {
         format_ref fr(fm(m));        
         pr(es[i], num_vars, var_prefix, fr, var_names);
-        fmts.push_back(fr);
+        fmts.push_back(std::move(fr));
     }
     r = mk_seq<format**, f2f>(m, fmts.c_ptr(), fmts.c_ptr() + fmts.size(), f2f());
 }

src/ast/fpa/fpa2bv_converter.cpp

@@ -3108,12 +3108,12 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
         expr_ref exp_bv(m), exp_all_ones(m);
         exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
         exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, ebits)));
-        m_extra_assertions.push_back(exp_all_ones);
+        m_extra_assertions.push_back(std::move(exp_all_ones));
 
         expr_ref sig_bv(m), sig_is_non_zero(m);
         sig_bv = m_bv_util.mk_extract(sbits-2, 0, result);
         sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1)));
-        m_extra_assertions.push_back(sig_is_non_zero);
+        m_extra_assertions.push_back(std::move(sig_is_non_zero));
     }
 
     TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;);

src/ast/rewriter/arith_rewriter.cpp

@@ -1159,49 +1159,44 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
         result = m_util.mk_numeral(floor(a), true);
         return BR_DONE;
     }
-    else if (m_util.is_to_real(arg, x)) {
+
+    if (m_util.is_to_real(arg, x)) {
         result = x;
         return BR_DONE;
     }
-    else {
-        if (m_util.is_add(arg) || m_util.is_mul(arg) || m_util.is_power(arg)) {
-            // Try to apply simplifications such as:
-            //    (to_int (+ 1.0 (to_real x))) --> (+ 1 x)
 
-            // if all arguments of arg are
+    if (m_util.is_add(arg) || m_util.is_mul(arg) || m_util.is_power(arg)) {
-            //   - integer numerals, OR
+        // Try to apply simplifications such as:
-            //   - to_real applications
+        //    (to_int (+ 1.0 (to_real x)) y) --> (+ 1 x (to_int y))
-            // then, to_int can be eliminated
+        
-            unsigned num_args = to_app(arg)->get_num_args();
+        expr_ref_buffer int_args(m()), real_args(m());
-            unsigned i = 0;
+        for (expr* c : *to_app(arg)) {
-            for (; i < num_args; i++) {
+            if (m_util.is_numeral(c, a) && a.is_int()) {
-                expr * c = to_app(arg)->get_arg(i);
+                int_args.push_back(m_util.mk_numeral(a, true));
-                if (m_util.is_numeral(c, a) && a.is_int())
-                    continue;
-                if (m_util.is_to_real(c))
-                    continue;
-                break; // failed
             }
-            if (i == num_args) {
+            else if (m_util.is_to_real(c, x)) {
-                // simplification can be applied
+                int_args.push_back(x);
-                expr_ref_buffer new_args(m());
+            }
-                for (i = 0; i < num_args; i++) {
+            else {
-                    expr * c = to_app(arg)->get_arg(i);
+                real_args.push_back(c);
-                    if (m_util.is_numeral(c, a) && a.is_int()) {
-                        new_args.push_back(m_util.mk_numeral(a, true));
-                    }
-                    else {
-                        VERIFY (m_util.is_to_real(c, x));
-                        new_args.push_back(x);
-                    }
-                }
-                SASSERT(num_args == new_args.size());
-                result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), new_args.size(), new_args.c_ptr());
-                return BR_REWRITE1;
             }
         }
-        return BR_FAILED;
+        if (real_args.empty()) {
+            result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), int_args.size(), int_args.c_ptr());
+            return BR_REWRITE1;
+        }
+        if (!int_args.empty() && (m_util.is_add(arg) || m_util.is_mul(arg))) {
+            decl_kind k = to_app(arg)->get_decl()->get_decl_kind();
+            expr_ref t1(m().mk_app(get_fid(), k, int_args.size(), int_args.c_ptr()), m());
+            expr_ref t2(m().mk_app(get_fid(), k, real_args.size(), real_args.c_ptr()), m());
+            int_args.reset();
+            int_args.push_back(t1);
+            int_args.push_back(m_util.mk_to_int(t2));
+            result = m().mk_app(get_fid(), k, int_args.size(), int_args.c_ptr());
+            return BR_REWRITE3;
+        }
     }
+    return BR_FAILED;
 }
 
 br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) {

src/ast/rewriter/bv_rewriter.cpp

@@ -1383,7 +1383,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
             --i;
             tmp = args[i].get();
             tmp = m_autil.mk_mul(m_autil.mk_numeral(power(numeral(2), sz), true), tmp);
-            args[i] = tmp;
+            args[i] = std::move(tmp);
             sz += get_bv_size(to_app(arg)->get_arg(i));
         }
         result = m_autil.mk_add(args.size(), args.c_ptr());
@@ -2400,8 +2400,8 @@ bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) {
         return false;
     }
     unsigned sz = to_app(rhs)->get_num_args();
-    expr_ref t1(m()), t2(m());
+    expr * t1 = to_app(rhs)->get_arg(0);
-    t1 = to_app(rhs)->get_arg(0);
+    expr_ref t2(m());
     if (sz > 2) {
         t2 = m().mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1);
     }
@@ -2597,14 +2597,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
                 result = m().mk_bool_val(new_lhs == new_rhs);
                 return BR_DONE;
             }
-        }
+            lhs = new_lhs;
-        else {
+            rhs = new_rhs;
-            new_lhs = lhs;
-            new_rhs = rhs;
         }
 
-        lhs = new_lhs;
-        rhs = new_rhs;
         // Try to rewrite t1 + t2 = c --> t1 = c - t2
         // Reason: it is much cheaper to bit-blast.
         if (isolate_term(lhs, rhs, result)) {

src/ast/rewriter/bv_trailing.cpp

@@ -125,7 +125,7 @@ struct bv_trailing::imp {
         for (unsigned i = 0; i < num; ++i) {
             expr * const curr = a->get_arg(i);
             VERIFY(to_rm == remove_trailing(curr, to_rm, tmp, depth - 1));
-            new_args.push_back(tmp);
+            new_args.push_back(std::move(tmp));
         }
         result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr());
         return to_rm;
@@ -150,7 +150,7 @@ struct bv_trailing::imp {
         numeral c_val;
         unsigned c_sz;
         if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one())
-            new_args.push_back(tmp);
+            new_args.push_back(std::move(tmp));
         const unsigned sz = m_util.get_bv_size(coefficient);
         const unsigned new_sz = sz - retv;
 
@@ -204,7 +204,7 @@ struct bv_trailing::imp {
         expr_ref_vector new_args(m);
         for (unsigned j = 0; j < i; ++j)
             new_args.push_back(a->get_arg(j));
-        if (new_last) new_args.push_back(new_last);
+        if (new_last) new_args.push_back(std::move(new_last));
         result = new_args.size() == 1 ? new_args.get(0)
                                       : m_util.mk_concat(new_args.size(), new_args.c_ptr());
         return retv;

src/ast/rewriter/th_rewriter.cpp

@@ -35,6 +35,7 @@ Notes:
 #include "ast/ast_util.h"
 #include "ast/well_sorted.h"
 
+namespace {
 struct th_rewriter_cfg : public default_rewriter_cfg {
     bool_rewriter       m_b_rw;
     arith_rewriter      m_a_rw;
@@ -337,16 +338,16 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         family_id fid = t->get_family_id();
         if (fid == m_a_rw.get_fid()) {
             switch (t->get_decl_kind()) {
-            case OP_ADD: n = m_a_util.mk_numeral(rational(0), m().get_sort(t)); return true;
+            case OP_ADD: n = m_a_util.mk_numeral(rational::zero(), m().get_sort(t)); return true;
-            case OP_MUL: n = m_a_util.mk_numeral(rational(1), m().get_sort(t)); return true;
+            case OP_MUL: n = m_a_util.mk_numeral(rational::one(), m().get_sort(t)); return true;
             default:
                 return false;
             }
         }
         if (fid == m_bv_rw.get_fid()) {
             switch (t->get_decl_kind()) {
-            case OP_BADD: n = m_bv_util.mk_numeral(rational(0), m().get_sort(t)); return true;
+            case OP_BADD: n = m_bv_util.mk_numeral(rational::zero(), m().get_sort(t)); return true;
-            case OP_BMUL: n = m_bv_util.mk_numeral(rational(1), m().get_sort(t)); return true;
+            case OP_BMUL: n = m_bv_util.mk_numeral(rational::one(), m().get_sort(t)); return true;
             default:
                 return false;
             }
@@ -468,9 +469,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         // terms matched...
         bool is_int = m_a_util.is_int(t1);
         if (!new_t1)
-            new_t1 = m_a_util.mk_numeral(rational(0), is_int);
+            new_t1 = m_a_util.mk_numeral(rational::zero(), is_int);
         if (!new_t2)
-            new_t2 = m_a_util.mk_numeral(rational(0), is_int);
+            new_t2 = m_a_util.mk_numeral(rational::zero(), is_int);
         // mk common part
         ptr_buffer<expr> args;
         for (unsigned i = 0; i < num1; i++) {
@@ -709,6 +710,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
 
 
 };
+}
 
 template class rewriter_tpl<th_rewriter_cfg>;
 
@@ -764,8 +766,8 @@ unsigned th_rewriter::get_num_steps() const {
 
 void th_rewriter::cleanup() {
     ast_manager & m = m_imp->m();
-    dealloc(m_imp);
+    m_imp->~imp();
-    m_imp = alloc(imp, m, m_params);
+    new (m_imp) imp(m, m_params);
 }
 
 void th_rewriter::reset() {

src/ast/substitution/substitution.cpp

@@ -196,16 +196,16 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
             expr_ref_vector pats(m_manager), no_pats(m_manager);
             for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
                 subst.apply(num_actual_offsets, deltas, expr_offset(q->get_pattern(i), off), s1, t1, er);
-                pats.push_back(er);
+                pats.push_back(std::move(er));
             }
             for (unsigned i = 0; i < q->get_num_no_patterns(); ++i) {
                 subst.apply(num_actual_offsets, deltas, expr_offset(q->get_no_pattern(i), off), s1, t1, er);
-                no_pats.push_back(er);
+                no_pats.push_back(std::move(er));
             }
             subst.apply(num_actual_offsets, deltas, body, s1, t1, er);
             er = m_manager.update_quantifier(q, pats.size(), pats.c_ptr(), no_pats.size(), no_pats.c_ptr(), er);
             m_todo.pop_back();
-            m_new_exprs.push_back(er);
+            m_new_exprs.push_back(std::move(er));
             m_apply_cache.insert(n, er);            
             break;
         }            

src/cmd_context/cmd_context.cpp

@@ -493,6 +493,7 @@ cmd_context::~cmd_context() {
     if (m_main_ctx) {
         set_verbose_stream(std::cerr);
     }
+    pop(m_scopes.size());
     finalize_cmds();
     finalize_tactic_cmds();
     finalize_probes();

src/cmd_context/pdecl.cpp

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include "cmd_context/pdecl.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/ast_pp.h"
 #include <sstream>
 using namespace format_ns;
 
@@ -768,9 +769,8 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
         }
         else {
             out << "(" << m_decl->get_name();
-            for (unsigned i = 0; i < m_args.size(); i++) {
+            for (auto arg : m_args) {
-                out << " ";
+                m.display(out << " ", arg);
-                m.display(out, m_args[i]);
             }
             out << ")";
         }
@@ -782,8 +782,8 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
         }
         else {
             ptr_buffer<format> b;
-            for (unsigned i = 0; i < m_args.size(); i++)
+            for (auto arg : m_args)
-                b.push_back(m.pp(m_args[i]));
+                b.push_back(m.pp(arg));
             return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str().c_str());
         }
     }
@@ -807,8 +807,8 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
         }
         else {
             out << "(_ " << m_decl->get_name();
-            for (unsigned i = 0; i < m_indices.size(); i++) {
+            for (auto idx : m_indices)  {
-                out << " " << m_indices[i];
+                out << " " << idx;
             }
             out << ")";
         }
@@ -821,8 +821,8 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
         else {
             ptr_buffer<format> b;
             b.push_back(mk_string(m.m(), m_decl->get_name().str().c_str()));
-            for (unsigned i = 0; i < m_indices.size(); i++)
+            for (auto idx : m_indices)
-                b.push_back(mk_unsigned(m.m(), m_indices[i]));
+                b.push_back(mk_unsigned(m.m(), idx));
             return mk_seq1(m.m(), b.begin(), b.end(), f2f(), "_");
         }
     }
@@ -853,6 +853,15 @@ pdecl_manager::pdecl_manager(ast_manager & m):
 pdecl_manager::~pdecl_manager() {
     dec_ref(m_list);
     reset_sort_info();
+    for (auto const& kv : m_sort2psort) {
+        del_decl_core(kv.m_value);
+        TRACE("pdecl_manager", tout << "orphan: " << mk_pp(kv.m_key, m()) << "\n";);
+    }
+    for (auto* p : m_table) {
+        del_decl_core(p);
+    }
+    m_sort2psort.reset();
+    m_table.reset();
     SASSERT(m_sort2psort.empty());
     SASSERT(m_table.empty());
 }
@@ -946,13 +955,15 @@ void pdecl_manager::del_decl_core(pdecl * p) {
 }
 
 void pdecl_manager::del_decl(pdecl * p) {
-    TRACE("register_psort", tout << "del psort "; p->display(tout); tout << "\n";);   
+    TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";);   
     if (p->is_psort()) {
         psort * _p = static_cast<psort*>(p);
-        if (_p->is_sort_wrapper())
+        if (_p->is_sort_wrapper()) {
             m_sort2psort.erase(static_cast<psort_sort*>(_p)->get_sort());
-        else
+        }
+        else {
             m_table.erase(_p);
+        }
     }
     del_decl_core(p);
 }

src/model/model.cpp

@@ -260,7 +260,7 @@ struct model::occs_collector {
     void operator()(func_decl* f) {
         ts.add_occurs(f);
     }
-    void operator()(ast* ) {}
+    void operator()(ast*) {}
 };
 
 
@@ -319,7 +319,7 @@ void model::collect_occs(top_sort& ts, func_decl* f) {
 
 void model::collect_occs(top_sort& ts, expr* e) {
     occs_collector collector(ts);
-    for_each_ast(collector, e);
+    for_each_ast(collector, e, true);
 }
 
 bool model::can_inline_def(top_sort& ts, func_decl* f) {

src/model/model_core.h

@@ -48,6 +48,14 @@ public:
     func_interp * get_func_interp(func_decl * d) const { func_interp * fi; return m_finterp.find(d, fi) ? fi : nullptr; }
 
     bool eval(func_decl * f, expr_ref & r) const;
+    bool is_true_decl(func_decl *f) const {
+        expr_ref r(m);
+        return eval(f, r) && m.is_true(r);
+    }
+    bool is_false_decl(func_decl *f) const {
+        expr_ref r(m);
+        return eval(f, r) && m.is_false(r);
+    }
 
     unsigned get_num_constants() const { return m_const_decls.size(); }
     unsigned get_num_functions() const { return m_func_decls.size(); }

src/muz/base/fp_params.pyg

@@ -150,6 +150,8 @@ def_module_params('fp',
                           ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'),
                           ('spacer.q3', BOOL, True, 'Allow quantified lemmas in frames'),
                           ('spacer.q3.instantiate', BOOL, True, 'Instantiate quantified lemmas'),
+                          ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'),
+                          ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'),
                           ('spacer.iuc', UINT, 1,
                            '0 = use old implementation of unsat-core-generation, ' +
                            '1 = use new implementation of IUC generation, ' +
@@ -160,13 +162,10 @@ def_module_params('fp',
                            '2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin'),
                           ('spacer.iuc.old_hyp_reducer', BOOL, False, 'use old hyp reducer instead of new implementation, for debugging only'),
                           ('spacer.validate_lemmas', BOOL, False, 'Validate each lemma after generalization'),
-                          ('spacer.reuse_pobs', BOOL, True, 'Reuse pobs'),
                           ('spacer.ground_pobs', BOOL, True, 'Ground pobs by using values from a model'),
                           ('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'),
                           ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'),
                           ('spacer.simplify_pob', BOOL, False, 'simplify pobs by removing redundant constraints'),
-                          ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'),
-                          ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'),
                           ('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'),
                           ('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"),
                           ('spacer.min_level', UINT, 0, 'Minimal level to explore'),

src/muz/spacer/spacer_context.cpp

@@ -55,6 +55,8 @@ Notes:
 
 #include "muz/spacer/spacer_sat_answer.h"
 
+#define WEAKNESS_MAX 65535
+
 namespace spacer {
 
 /// pob -- proof obligation
@@ -66,8 +68,8 @@ pob::pob (pob* parent, pred_transformer& pt,
     m_binding(m_pt.get_ast_manager()),
     m_new_post (m_pt.get_ast_manager ()),
     m_level (level), m_depth (depth),
-    m_open (true), m_use_farkas (true), m_weakness(0),
+    m_open (true), m_use_farkas (true), m_in_queue(false),
-    m_blocked_lvl(0) {
+    m_weakness(0), m_blocked_lvl(0) {
     if (add_to_parent && m_parent) {
         m_parent->add_child(*this);
     }
@@ -79,6 +81,7 @@ void pob::set_post(expr* post) {
 }
 
 void pob::set_post(expr* post, app_ref_vector const &binding) {
+    SASSERT(!is_in_queue());
     normalize(post, m_post,
               m_pt.get_context().simplify_pob(),
               m_pt.get_context().use_euf_gen());
@@ -88,6 +91,7 @@ void pob::set_post(expr* post, app_ref_vector const &binding) {
 }
 
 void pob::inherit(pob const &p) {
+    SASSERT(!is_in_queue());
     SASSERT(m_parent == p.m_parent);
     SASSERT(&m_pt == &p.m_pt);
     SASSERT(m_post == p.m_post);
@@ -105,17 +109,10 @@ void pob::inherit(pob const &p) {
     m_derivation = nullptr;
 }
 
-void pob::clean () {
-    if (m_new_post) {
-        m_post = m_new_post;
-        m_new_post.reset();
-    }
-}
-
 void pob::close () {
     if (!m_open) { return; }
 
-    reset ();
+    m_derivation = nullptr;
     m_open = false;
     for (unsigned i = 0, sz = m_kids.size (); i < sz; ++i)
     { m_kids [i]->close(); }
@@ -129,7 +126,15 @@ void pob::get_skolems(app_ref_vector &v) {
     }
 }
 
-
+    std::ostream &pob::display(std::ostream &out, bool full) const {
+        out << pt().head()->get_name ()
+            << " level: " << level()
+            << " depth: " << depth()
+            << " post_id: " << post()->get_id()
+            << (is_in_queue() ? " in_queue" : "");
+        if (full) out << "\n" << m_post;
+        return out;
+    }
 
 // ----------------
 // pob_queue
@@ -137,17 +142,24 @@ void pob::get_skolems(app_ref_vector &v) {
 pob* pob_queue::top ()
 {
     /// nothing in the queue
-    if (m_obligations.empty()) { return nullptr; }
+    if (m_data.empty()) { return nullptr; }
     /// top queue element is above max level
-    if (m_obligations.top()->level() > m_max_level) { return nullptr; }
+    if (m_data.top()->level() > m_max_level) { return nullptr; }
     /// top queue element is at the max level, but at a higher than base depth
-    if (m_obligations.top ()->level () == m_max_level &&
+    if (m_data.top ()->level () == m_max_level &&
-        m_obligations.top()->depth() > m_min_depth) { return nullptr; }
+        m_data.top()->depth() > m_min_depth) { return nullptr; }
 
     /// there is something good in the queue
-    return m_obligations.top ().get ();
+    return m_data.top ();
 }
 
+void pob_queue::pop() {
+    pob *p = m_data.top();
+    p->set_in_queue(false);
+    m_data.pop();
+}
+
+
 void pob_queue::set_root(pob& root)
 {
     m_root = &root;
@@ -156,19 +168,28 @@ void pob_queue::set_root(pob& root)
     reset();
 }
 
-pob_queue::~pob_queue() {}
-
 void pob_queue::reset()
 {
-    while (!m_obligations.empty()) { m_obligations.pop(); }
+    while (!m_data.empty()) {
-    if (m_root) { m_obligations.push(m_root); }
+        pob *p = m_data.top();
+        m_data.pop();
+        p->set_in_queue(false);
+    }
+    if (m_root) {
+        SASSERT(!m_root->is_in_queue());
+        m_root->set_in_queue(true);
+        m_data.push(m_root.get());
+    }
 }
 
 void pob_queue::push(pob &n) {
-    TRACE("pob_queue",
+    if (!n.is_in_queue()) {
-          tout << "pob_queue::push(" << n.post()->get_id() << ")\n";);
+        TRACE("pob_queue",
-    m_obligations.push (&n);
+              tout << "pob_queue::push(" << n.post()->get_id() << ")\n";);
-    n.get_context().new_pob_eh(&n);
+        n.set_in_queue(true);
+        m_data.push (&n);
+        n.get_context().new_pob_eh(&n);
+    }
 }
 
 // ----------------
@@ -266,6 +287,8 @@ pob *derivation::create_next_child(model &mdl)
         m_evars.reset();
         pt().mbp(vars, m_trans, mdl,
                  true, pt().get_context().use_ground_pob());
+        CTRACE("spacer", !vars.empty(),
+               tout << "Failed to eliminate: " << vars << "\n";);
         m_evars.append (vars);
         vars.reset();
     }
@@ -295,6 +318,8 @@ pob *derivation::create_next_child(model &mdl)
         vars.append(m_evars);
         pt().mbp(vars, post, mdl,
                  true, pt().get_context().use_ground_pob());
+        CTRACE("spacer", !vars.empty(),
+               tout << "Failed to eliminate: " << vars << "\n";);
         //qe::reduce_array_selects (*mev.get_model (), post);
     }
     else {
@@ -398,6 +423,8 @@ pob *derivation::create_next_child ()
             this->pt().mbp(vars, m_trans, *mdl,
                            true, this->pt().get_context().use_ground_pob());
             // keep track of implicitly quantified variables
+            CTRACE("spacer", !vars.empty(),
+                   tout << "Failed to eliminate: " << vars << "\n";);
             m_evars.append (vars);
             vars.reset();
         }
@@ -462,8 +489,11 @@ void derivation::premise::set_summary (expr * summary, bool must,
 lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
     m_ref_count(0), m(manager),
     m_body(body, m), m_cube(m),
-    m_zks(m), m_bindings(m), m_lvl(lvl), m_init_lvl(m_lvl),
+    m_zks(m), m_bindings(m),
-    m_pob(nullptr), m_ctp(nullptr), m_external(false), m_bumped(0) {
+    m_pob(nullptr), m_ctp(nullptr),
+    m_lvl(lvl), m_init_lvl(m_lvl),
+    m_bumped(0), m_weakness(WEAKNESS_MAX),
+    m_external(false), m_blocked(false) {
     SASSERT(m_body);
     normalize(m_body, m_body);
 }
@@ -471,8 +501,11 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
 lemma::lemma(pob_ref const &p) :
     m_ref_count(0), m(p->get_ast_manager()),
     m_body(m), m_cube(m),
-    m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl),
+    m_zks(m), m_bindings(m),
-    m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0) {
+    m_pob(p), m_ctp(nullptr),
+    m_lvl(p->level()), m_init_lvl(m_lvl),
+    m_bumped(0), m_weakness(p->weakness()),
+    m_external(false), m_blocked(false) {
     SASSERT(m_pob);
     m_pob->get_skolems(m_zks);
     add_binding(m_pob->get_binding());
@@ -482,8 +515,11 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) :
     m_ref_count(0),
     m(p->get_ast_manager()),
     m_body(m), m_cube(m),
-    m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl),
+    m_zks(m), m_bindings(m),
-    m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0)
+    m_pob(p), m_ctp(nullptr),
+    m_lvl(p->level()), m_init_lvl(m_lvl),
+    m_bumped(0), m_weakness(p->weakness()),
+    m_external(false), m_blocked(false)
 {
     if (m_pob) {
         m_pob->get_skolems(m_zks);
@@ -510,7 +546,8 @@ void lemma::mk_expr_core() {
     SASSERT(!m_cube.empty());
     m_body = ::mk_and(m_cube);
     // normalize works better with a cube
-    normalize(m_body, m_body);
+    normalize(m_body, m_body, false /* no simplify bounds */, false /* term_graph */);
+
     m_body = ::push_not(m_body);
 
     if (!m_zks.empty() && has_zk_const(m_body)) {
@@ -820,7 +857,7 @@ const datalog::rule *pred_transformer::find_rule(model &model) {
 
     for (auto &kv : m_pt_rules) {
         app *tag = kv.m_value->tag();
-        if (model.eval(tag->get_decl(), val) && m.is_true(val)) {
+        if (model.is_true_decl(tag->get_decl())) {
             return &kv.m_value->rule();
         }
     }
@@ -1162,7 +1199,16 @@ expr_ref pred_transformer::get_origin_summary (model &mdl,
     }
 
     // bail out of if the model is insufficient
-    if (!mdl.is_true(summary)) return expr_ref(m);
+    // (skip quantified lemmas cause we can't validate them in the model)
+    // TBD: for quantified lemmas use current instances
+    flatten_and(summary);
+    for (auto *s : summary) {
+        if (!is_quantifier(s) && !mdl.is_true(s)) {
+            TRACE("spacer", tout << "Summary not true in the model: "
+                  << mk_pp(s, m) << "\n";);
+            return expr_ref(m);
+        }
+    }
 
     // -- pick an implicant
     expr_ref_vector lits(m);
@@ -1347,7 +1393,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
 
     if (is_sat == l_true || is_sat == l_undef) {
         if (core) { core->reset(); }
-        if (model) {
+        if (model && model->get()) {
             r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach);
             TRACE ("spacer", tout << "reachable "
                    << "is_concrete " << is_concrete << " rused: ";
@@ -1387,7 +1433,12 @@ bool pred_transformer::is_ctp_blocked(lemma *lem) {
     // -- find rule of the ctp
     const datalog::rule *r;
     r = find_rule(*ctp);
-    if (r == nullptr) {return false;}
+    if (r == nullptr) {
+        // no rules means lemma is blocked forever because
+        // it does not satisfy some derived facts
+        lem->set_blocked(true);
+        return true;
+    }
 
     // -- find predicates along the rule
     find_predecessors(*r, m_predicates);
@@ -1410,6 +1461,8 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
                                     unsigned& solver_level,
                                     expr_ref_vector* core)
 {
+    if (lem->is_blocked()) return false;
+
     m_stats.m_num_is_invariant++;
     if (is_ctp_blocked(lem)) {
         m_stats.m_num_ctp_blocked++;
@@ -1451,7 +1504,7 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
         SASSERT (level <= solver_level);
     }
     else if (r == l_true) {
-        // optionally remove unused symbols from the model
+        // TBD: optionally remove unused symbols from the model
         if (mdl_ref_ptr) {lem->set_ctp(*mdl_ref_ptr);}
     }
     else {lem->reset_ctp();}
@@ -2120,25 +2173,17 @@ void pred_transformer::frames::simplify_formulas ()
 
 /// pred_transformer::pobs
 
-pob* pred_transformer::pobs::mk_pob(pob *parent,
+pob* pred_transformer::pob_manager::mk_pob(pob *parent,
-                                    unsigned level, unsigned depth,
+                                           unsigned level, unsigned depth,
-                                    expr *post, app_ref_vector const &b) {
+                                           expr *post,
-
+                                           app_ref_vector const &b) {
-    if (!m_pt.ctx.reuse_pobs()) {
-        pob* n = alloc(pob, parent, m_pt, level, depth);
-        n->set_post(post, b);
-        return n;
-    }
-
     // create a new pob and set its post to normalize it
     pob p(parent, m_pt, level, depth, false);
     p.set_post(post, b);
 
     if (m_pobs.contains(p.post())) {
-        auto &buf = m_pobs[p.post()];
+        for (auto *f : m_pobs[p.post()]) {
-        for (unsigned i = 0, sz = buf.size(); i < sz; ++i) {
+            if (f->parent() == parent && !f->is_in_queue()) {
-            pob *f = buf.get(i);
-            if (f->parent() == parent) {
                 f->inherit(p);
                 return f;
             }
@@ -2160,7 +2205,21 @@ pob* pred_transformer::pobs::mk_pob(pob *parent,
     return n;
 }
 
-
+pob* pred_transformer::pob_manager::find_pob(pob* parent, expr *post) {
+    pob p(parent, m_pt, 0, 0, false);
+    p.set_post(post);
+    pob *res = nullptr;
+    if (m_pobs.contains(p.post())) {
+        for (auto *f : m_pobs[p.post()]) {
+            if (f->parent() == parent) {
+                // try to find pob not already in queue
+                if (!f->is_in_queue()) return f;
+                res = f;
+            }
+        }
+    }
+    return res;
+}
 
 
 // ----------------
@@ -2207,7 +2266,6 @@ void context::updt_params() {
     m_use_ctp = m_params.spacer_ctp();
     m_use_inc_clause = m_params.spacer_use_inc_clause();
     m_blast_term_ite = m_params.spacer_blast_term_ite();
-    m_reuse_pobs = m_params.spacer_reuse_pobs();
     m_use_ind_gen = m_params.spacer_use_inductive_generalizer();
     m_use_array_eq_gen = m_params.spacer_use_array_eq_generalizer();
     m_validate_lemmas = m_params.spacer_validate_lemmas();
@@ -3055,27 +3113,19 @@ bool context::check_reachability ()
         }
 
         SASSERT (m_pob_queue.top ());
-        // -- remove all closed nodes and updated all dirty nodes
+        // -- remove all closed nodes
         // -- this is necessary because there is no easy way to
         // -- remove nodes from the priority queue.
-        while (m_pob_queue.top ()->is_closed () ||
+        while (m_pob_queue.top ()->is_closed ()) {
-               m_pob_queue.top()->is_dirty()) {
+            pob_ref n = m_pob_queue.top();
-            pob_ref n = m_pob_queue.top ();
+            m_pob_queue.pop();
-            m_pob_queue.pop ();
+            IF_VERBOSE (1,
-            if (n->is_closed()) {
+                        verbose_stream () << "Deleting closed node: "
-                IF_VERBOSE (1,
+                        << n->pt ().head ()->get_name ()
-                            verbose_stream () << "Deleting closed node: "
+                        << "(" << n->level () << ", " << n->depth () << ")"
-                            << n->pt ().head ()->get_name ()
+                        << " " << n->post ()->get_id () << "\n";);
-                            << "(" << n->level () << ", " << n->depth () << ")"
+            if (m_pob_queue.is_root(*n)) {return true;}
-                            << " " << n->post ()->get_id () << "\n";);
+            SASSERT (m_pob_queue.top ());
-                if (m_pob_queue.is_root(*n)) { return true; }
-                SASSERT (m_pob_queue.top ());
-            } else if (n->is_dirty()) {
-                n->clean ();
-                // -- the node n might not be at the top after it is cleaned
-                m_pob_queue.push (*n);
-            } else
-            { UNREACHABLE(); }
         }
 
         SASSERT (m_pob_queue.top ());
@@ -3169,6 +3219,7 @@ bool context::is_reachable(pob &n)
     unsigned num_reuse_reach = 0;
 
     unsigned saved = n.level ();
+    // TBD: don't expose private field
     n.m_level = infty_level ();
     lbool res = n.pt().is_reachable(n, nullptr, &mdl,
                                     uses_level, is_concrete, r,
@@ -3413,10 +3464,21 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
 
         // Optionally update the node to be the negation of the lemma
         if (v && m_use_lemma_as_pob) {
-            n.new_post (mk_and(lemma->get_cube()));
+            expr_ref c(m);
-            n.set_farkas_generalizer (false);
+            c = mk_and(lemma->get_cube());
-            // XXX hack while refactoring is in progress
+            // check that the post condition is different
-            n.clean();
+            if (c  != n.post()) {
+                pob *f = n.pt().find_pob(n.parent(), c);
+                // skip if a similar pob is already in the queue
+                if (f != &n && (!f || !f->is_in_queue())) {
+                    f = n.pt().mk_pob(n.parent(), n.level(),
+                                      n.depth(), c, n.get_binding());
+                    SASSERT(!f->is_in_queue());
+                    f->inc_level();
+                    //f->set_farkas_generalizer(false);
+                    out.push_back(f);
+                }
+            }
         }
 
         // schedule the node to be placed back in the queue
@@ -3434,7 +3496,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
     }
     case l_undef:
         // something went wrong
-        if (n.weakness() < 100 /* MAX_WEAKENSS */) {
+        if (n.weakness() < 10 /* MAX_WEAKENSS */) {
             bool has_new_child = false;
             SASSERT(m_weak_abs);
             m_stats.m_expand_pob_undef++;
@@ -3932,7 +3994,7 @@ bool context::is_inductive() {
 }
 
 /// pob_lt operator
-inline bool pob_lt::operator() (const pob *pn1, const pob *pn2) const
+inline bool pob_lt_proc::operator() (const pob *pn1, const pob *pn2) const
 {
     SASSERT (pn1);
     SASSERT (pn2);

src/muz/spacer/spacer_context.h

@@ -122,12 +122,14 @@ class lemma {
     expr_ref_vector m_cube;
     app_ref_vector m_zks;
     app_ref_vector m_bindings;
+    pob_ref m_pob;
+    model_ref m_ctp;           // counter-example to pushing
     unsigned m_lvl;            // current level of the lemma
     unsigned m_init_lvl;       // level at which lemma was created
-    pob_ref m_pob;
+    unsigned m_bumped:16;
-    model_ref m_ctp; // counter-example to pushing
+    unsigned m_weakness:16;
-    bool m_external;
+    unsigned m_external:1;
-    unsigned m_bumped;
+    unsigned m_blocked:1;
 
     void mk_expr_core();
     void mk_cube_core();
@@ -154,12 +156,15 @@ public:
 
     bool has_pob() {return m_pob;}
     pob_ref &get_pob() {return m_pob;}
-    inline unsigned weakness();
+    unsigned weakness() {return m_weakness;}
 
     void add_skolem(app *zk, app* b);
 
-    inline void set_external(bool ext){m_external = ext;}
+    void set_external(bool ext){m_external = ext;}
-    inline bool external() { return m_external;}
+    bool external() { return m_external;}
+
+    bool is_blocked() {return m_blocked;}
+    void set_blocked(bool v) {m_blocked=v;}
 
     bool is_inductive() const {return is_infty_level(m_lvl);}
     unsigned level () const {return m_lvl;}
@@ -268,18 +273,31 @@ class pred_transformer {
     };
 
     /**
-        manager of proof-obligations (pobs)
+        manager of proof-obligations (pob_manager)
+
+        Pobs are determined uniquely by their post-condition and a parent pob.
+        They are managed by pob_manager and remain live through the
+        life of the manager
      */
-    class pobs {
+    class pob_manager {
+        // a buffer that contains space for one pob and allocates more
+        // space if needed
         typedef ptr_buffer<pob, 1> pob_buffer;
+        // Type for the map from post-conditions to pobs. The common
+        // case is that each post-condition corresponds to a single
+        // pob. Other cases are handled by expanding the buffer
         typedef obj_map<expr, pob_buffer > expr2pob_buffer;
 
+        // parent predicate transformer
         pred_transformer &m_pt;
 
+        // map from post-conditions to pobs
         expr2pob_buffer m_pobs;
+
+        // a store
         pob_ref_vector m_pinned;
     public:
-        pobs(pred_transformer &pt) : m_pt(pt) {}
+        pob_manager(pred_transformer &pt) : m_pt(pt) {}
         pob* mk_pob(pob *parent, unsigned level, unsigned depth,
                     expr *post, app_ref_vector const &b);
 
@@ -290,6 +308,7 @@ class pred_transformer {
         }
         unsigned size() const {return m_pinned.size();}
 
+        pob* find_pob(pob* parent, expr *post);
     };
 
     class pt_rule {
@@ -361,7 +380,7 @@ class pred_transformer {
     ptr_vector<datalog::rule>    m_rules;           // rules used to derive transformer
     scoped_ptr<prop_solver>      m_solver;          // solver context
     ref<solver>                  m_reach_solver;       // context for reachability facts
-    pobs                         m_pobs;            // proof obligations created so far
+    pob_manager                         m_pobs;            // proof obligations created so far
     frames                       m_frames;          // frames with lemmas
     reach_fact_ref_vector        m_reach_facts;     // reach facts
     unsigned                     m_rf_init_sz;      // number of reach fact from INIT
@@ -481,6 +500,9 @@ public:
                 expr *post, app_ref_vector const &b){
         return m_pobs.mk_pob(parent, level, depth, post, b);
     }
+    pob* find_pob(pob *parent, expr *post) {
+        return m_pobs.find_pob(parent, post);
+    }
 
     pob* mk_pob(pob *parent, unsigned level, unsigned depth,
                 expr *post) {
@@ -548,6 +570,7 @@ public:
  * A proof obligation.
  */
 class pob {
+    // TBD: remove this
     friend class context;
     unsigned m_ref_count;
     /// parent node
@@ -562,14 +585,15 @@ class pob {
     /// new post to be swapped in for m_post
     expr_ref                m_new_post;
     /// level at which to decide the post
-    unsigned                m_level;
+    unsigned                m_level:16;
-
+    unsigned                m_depth:16;
-    unsigned                m_depth;
 
     /// whether a concrete answer to the post is found
-    bool                    m_open;
+    unsigned                m_open:1;
     /// whether to use farkas generalizer to construct a lemma blocking this node
-    bool                    m_use_farkas;
+    unsigned                m_use_farkas:1;
+    /// true if this pob is in pob_queue
+    unsigned                m_in_queue:1;
 
     unsigned                m_weakness;
     /// derivation representing the position of this node in the parent's rule
@@ -584,17 +608,25 @@ class pob {
     // depth -> watch
     std::map<unsigned, stopwatch> m_expand_watches;
     unsigned m_blocked_lvl;
+
 public:
     pob (pob* parent, pred_transformer& pt,
          unsigned level, unsigned depth=0, bool add_to_parent=true);
 
     ~pob() {if (m_parent) { m_parent->erase_child(*this); }}
 
+    // TBD: move into constructor and make private
+    void set_post(expr *post, app_ref_vector const &binding);
+    void set_post(expr *post);
+
     unsigned weakness() {return m_weakness;}
     void bump_weakness() {m_weakness++;}
     void reset_weakness() {m_weakness=0;}
 
-    void inc_level () {m_level++; m_depth++;reset_weakness();}
+    void inc_level () {
+        SASSERT(!is_in_queue());
+        m_level++; m_depth++;reset_weakness();
+    }
 
     void inherit(pob const &p);
     void set_derivation (derivation *d) {m_derivation = d;}
@@ -614,32 +646,25 @@ public:
     unsigned level () const { return m_level; }
     unsigned depth () const {return m_depth;}
     unsigned width () const {return m_kids.size();}
-    unsigned blocked_at(unsigned lvl=0){return (m_blocked_lvl = std::max(lvl, m_blocked_lvl)); }
+    unsigned blocked_at(unsigned lvl=0){
+        return (m_blocked_lvl = std::max(lvl, m_blocked_lvl));
+    }
 
+    bool is_in_queue() const {return m_in_queue;}
+    void set_in_queue(bool v) {m_in_queue = v;}
     bool use_farkas_generalizer () const {return m_use_farkas;}
     void set_farkas_generalizer (bool v) {m_use_farkas = v;}
 
     expr* post() const { return m_post.get (); }
-    void set_post(expr *post);
-    void set_post(expr *post, app_ref_vector const &binding);
-
-    /// indicate that a new post should be set for the node
-    void new_post(expr *post) {if (post != m_post) {m_new_post = post;}}
-    /// true if the node needs to be updated outside of the priority queue
-    bool is_dirty () {return m_new_post;}
-    /// clean a dirty node
-    void clean();
-
-    void reset () {clean (); m_derivation = nullptr; m_open = true;}
 
     bool is_closed () const { return !m_open; }
     void close();
 
-    const ptr_vector<pob> &children() {return m_kids;}
+    const ptr_vector<pob> &children() const {return m_kids;}
     void add_child (pob &v) {m_kids.push_back (&v);}
     void erase_child (pob &v) {m_kids.erase (&v);}
 
-    const ptr_vector<lemma> &lemmas() {return m_lemmas;}
+    const ptr_vector<lemma> &lemmas() const {return m_lemmas;}
     void add_lemma(lemma* new_lemma) {m_lemmas.push_back(new_lemma);}
 
     bool is_ground () const { return m_binding.empty (); }
@@ -652,8 +677,14 @@ public:
      */
     void get_skolems(app_ref_vector& v);
 
-    void on_expand() { m_expand_watches[m_depth].start(); if (m_parent.get()){m_parent.get()->on_expand();} }
+    void on_expand() {
-    void off_expand() { m_expand_watches[m_depth].stop(); if (m_parent.get()){m_parent.get()->off_expand();} };
+        m_expand_watches[m_depth].start();
+        if (m_parent.get()){m_parent.get()->on_expand();}
+    }
+    void off_expand() {
+        m_expand_watches[m_depth].stop();
+        if (m_parent.get()){m_parent.get()->off_expand();}
+    }
     double get_expand_time(unsigned depth) { return m_expand_watches[depth].get_seconds();}
 
     void inc_ref () {++m_ref_count;}
@@ -662,6 +693,7 @@ public:
         if (m_ref_count == 0) {dealloc(this);}
     }
 
+    std::ostream &display(std::ostream &out, bool full = false) const;
     class on_expand_event
     {
         pob &m_p;
@@ -671,26 +703,20 @@ public:
     };
 };
 
+inline std::ostream &operator<<(std::ostream &out, pob const &p) {
+    return p.display(out);
+}
 
-struct pob_lt :
+struct pob_lt_proc : public std::binary_function<const pob*, const pob*, bool> {
-        public std::binary_function<const pob*, const pob*, bool>
+    bool operator() (const pob *pn1, const pob *pn2) const;
-{bool operator() (const pob *pn1, const pob *pn2) const;};
-
-struct pob_gt :
-        public std::binary_function<const pob*, const pob*, bool> {
-    pob_lt lt;
-    bool operator() (const pob *n1, const pob *n2) const
-        {return lt(n2, n1);}
 };
 
-struct pob_ref_gt :
+struct pob_gt_proc : public std::binary_function<const pob*, const pob*, bool> {
-        public std::binary_function<const pob_ref&, const model_ref &, bool> {
+    bool operator() (const pob *n1, const pob *n2) const {
-    pob_gt gt;
+        return pob_lt_proc()(n2, n1);
-    bool operator() (const pob_ref &n1, const pob_ref &n2) const
+    }
-        {return gt (n1.get (), n2.get ());}
 };
 
-inline unsigned lemma::weakness() {return m_pob ? m_pob->weakness() : UINT_MAX;}
 /**
  */
 class derivation {
@@ -767,36 +793,41 @@ public:
 
 
 class pob_queue {
+
+    typedef std::priority_queue<pob*, std::vector<pob*>, pob_gt_proc> pob_queue_ty;
     pob_ref  m_root;
     unsigned m_max_level;
     unsigned m_min_depth;
 
-    std::priority_queue<pob_ref, std::vector<pob_ref>,
+    pob_queue_ty  m_data;
-                        pob_ref_gt>     m_obligations;
 
 public:
     pob_queue(): m_root(nullptr), m_max_level(0), m_min_depth(0) {}
-    ~pob_queue();
+    ~pob_queue() {}
 
     void reset();
-    pob * top ();
+    pob* top();
-    void pop () {m_obligations.pop ();}
+    void pop();
     void push (pob &n);
 
     void inc_level () {
-        SASSERT (!m_obligations.empty () || m_root);
+        SASSERT (!m_data.empty () || m_root);
         m_max_level++;
         m_min_depth++;
-        if (m_root && m_obligations.empty()) { m_obligations.push(m_root); }
+        if (m_root && m_data.empty()) {
+            SASSERT(!m_root->is_in_queue());
+            m_root->set_in_queue(true);
+            m_data.push(m_root.get());
+        }
     }
 
     pob& get_root() const {return *m_root.get ();}
     void set_root(pob& n);
-    bool is_root (pob& n) const {return m_root.get () == &n;}
+    bool is_root(pob& n) const {return m_root.get () == &n;}
 
     unsigned max_level() const {return m_max_level;}
     unsigned min_depth() const {return m_min_depth;}
-    size_t size() const {return m_obligations.size();}
+    size_t size() const {return m_data.size();}
 };
 
 
@@ -910,7 +941,6 @@ class context {
     bool                 m_use_ctp;
     bool                 m_use_inc_clause;
     bool                 m_blast_term_ite;
-    bool                 m_reuse_pobs;
     bool                 m_use_ind_gen;
     bool                 m_use_array_eq_gen;
     bool                 m_validate_lemmas;
@@ -1007,7 +1037,6 @@ public:
     bool use_ctp() {return m_use_ctp;}
     bool use_inc_clause() {return m_use_inc_clause;}
     bool blast_term_ite() {return m_blast_term_ite;}
-    bool reuse_pobs() {return m_reuse_pobs;}
     bool elim_aux() {return m_elim_aux;}
     bool reach_dnf() {return m_reach_dnf;}
 

src/muz/spacer/spacer_iuc_solver.cpp

@@ -322,6 +322,24 @@ void iuc_solver::get_iuc(expr_ref_vector &core)
         // -- new hypothesis reducer
         else
         {
+#if 0
+            static unsigned bcnt = 0;
+            {
+                bcnt++;
+                TRACE("spacer", tout << "Dumping pf bcnt: " << bcnt << "\n";);
+                if (bcnt == 123) {
+                    std::ofstream ofs;
+                    ofs.open("/tmp/bpf_" + std::to_string(bcnt) + ".dot");
+                    iuc_proof iuc_pf_before(m, res.get(), core_lits);
+                    iuc_pf_before.display_dot(ofs);
+                    ofs.close();
+
+                    proof_checker pc(m);
+                    expr_ref_vector side(m);
+                    ENSURE(pc.check(res, side));
+                }
+            }
+#endif
             scoped_watch _t_ (m_hyp_reduce2_sw);
 
             // pre-process proof for better iuc extraction
@@ -356,6 +374,22 @@ void iuc_solver::get_iuc(expr_ref_vector &core)
 
         iuc_proof iuc_pf(m, res, core_lits);
 
+#if 0
+        static unsigned cnt = 0;
+        {
+            cnt++;
+            TRACE("spacer", tout << "Dumping pf cnt: " << cnt << "\n";);
+            if (cnt == 123) {
+                std::ofstream ofs;
+                ofs.open("/tmp/pf_" + std::to_string(cnt) + ".dot");
+                iuc_pf.display_dot(ofs);
+                ofs.close();
+                proof_checker pc(m);
+                expr_ref_vector side(m);
+                ENSURE(pc.check(res, side));
+            }
+        }
+#endif
         unsat_core_learner learner(m, iuc_pf);
 
         unsat_core_plugin* plugin;

src/muz/spacer/spacer_prop_solver.cpp

@@ -56,6 +56,7 @@ prop_solver::prop_solver(ast_manager &m,
     m_use_push_bg(p.spacer_keep_proxy())
 {
 
+    m_random.set_seed(p.spacer_random_seed());
     m_solvers[0] = solver0;
     m_solvers[1] = solver1;
 
@@ -363,6 +364,8 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
     hard.append(_hard.size(), _hard.c_ptr());
     flatten_and(hard);
 
+    shuffle(hard.size(), hard.c_ptr(), m_random);
+
     m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get();
 
     // can be disabled if use_push_bg == true

src/muz/spacer/spacer_prop_solver.h

@@ -61,6 +61,8 @@ private:
     bool                m_use_push_bg;
     unsigned            m_current_level;    // set when m_in_level
 
+    random_gen          m_random;
+
     void assert_level_atoms(unsigned level);
 
     void ensure_level(unsigned lvl);

src/muz/spacer/spacer_quant_generalizer.cpp

@@ -80,6 +80,51 @@ struct index_lt_proc : public std::binary_function<app*, app *, bool> {
     }
 };
 
+
+    struct has_nlira_functor {
+        struct found{};
+
+        ast_manager &m;
+        arith_util   u;
+
+        has_nlira_functor(ast_manager &_m) : m(_m), u(m) {}
+
+        void operator()(var *) {}
+        void operator()(quantifier *) {}
+        void operator()(app *n) {
+            family_id fid = n->get_family_id();
+            if (fid != u.get_family_id()) return;
+
+            switch(n->get_decl_kind()) {
+            case OP_MUL:
+                if (n->get_num_args() != 2)
+                    throw found();
+                if (!u.is_numeral(n->get_arg(0)) && !u.is_numeral(n->get_arg(1)))
+                    throw found();
+                return;
+            case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
+                if (!u.is_numeral(n->get_arg(1)))
+                    throw found();
+                return;
+            default:
+                return;
+            }
+            return;
+        }
+    };
+
+    bool has_nlira(expr_ref_vector &v) {
+        has_nlira_functor fn(v.m());
+        expr_fast_mark1 visited;
+        try {
+            for (expr *e : v)
+                quick_for_each_expr(fn, visited, e);
+        }
+        catch (has_nlira_functor::found e) {
+            return true;
+        }
+        return false;
+    }
 }
 
 namespace spacer {
@@ -114,7 +159,7 @@ void lemma_quantifier_generalizer::find_candidates(expr *e,
     if (!contains_selects(e, m)) return;
 
     app_ref_vector indices(m);
-    get_select_indices(e, indices, m);
+    get_select_indices(e, indices);
 
     app_ref_vector extra(m);
     expr_sparse_mark marked_args;
@@ -155,7 +200,7 @@ bool lemma_quantifier_generalizer::match_sk_idx(expr *e, app_ref_vector const &z
 
     if (!contains_selects(e, m)) return false;
     app_ref_vector indicies(m);
-    get_select_indices(e, indicies, m);
+    get_select_indices(e, indicies);
     if (indicies.size() > 2) return false;
 
     unsigned i=0;
@@ -191,9 +236,15 @@ expr* times_minus_one(expr *e, arith_util &arith) {
     Find sub-expression of the form (select A (+ sk!0 t)) and replaces
     (+ sk!0 t) --> sk!0 and sk!0 --> (+ sk!0 (* (- 1) t))
 
-    Current implementation is an ugly hack for one special case
+
+    rewrites bind to  (+ bsk!0 t) where bsk!0 is the original binding for sk!0
+
+    Current implementation is an ugly hack for one special
+    case. Should be rewritten based on an equality solver from qe
 */
-void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector const &zks, expr_ref &bind) {
+void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube,
+                                           app_ref_vector const &zks,
+                                           expr_ref &bind) {
     if (zks.size() != 1) return;
 
     arith_util arith(m);
@@ -219,8 +270,8 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector
                     kids_bind.push_back(bind);
                 }
                 else {
-                    kids.push_back (times_minus_one(arg, arith));
+                    kids.push_back(times_minus_one(arg, arith));
-                    kids_bind.push_back (times_minus_one(arg, arith));
+                    kids_bind.push_back(arg);
                 }
             }
             if (!found) continue;
@@ -228,7 +279,8 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector
             rep = arith.mk_add(kids.size(), kids.c_ptr());
             bind = arith.mk_add(kids_bind.size(), kids_bind.c_ptr());
             TRACE("spacer_qgen",
-                  tout << "replace " << mk_pp(idx, m) << " with " << mk_pp(rep, m) << "\n";);
+                  tout << "replace " << mk_pp(idx, m) << " with " << mk_pp(rep, m) << "\n"
+                  << "bind is: " << bind << "\n";);
             break;
         }
     }
@@ -255,15 +307,17 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector
 
    lb and ub are null if no bound was found
  */
-void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, var *var,
+void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term,
+                                               var *var,
                                                expr_ref_vector &gnd_cube,
                                                expr_ref_vector &abs_cube,
-                                               expr *&lb, expr *&ub, unsigned &stride) {
+                                               expr *&lb, expr *&ub,
+                                               unsigned &stride) {
 
     // create an abstraction function that maps candidate term to variables
     expr_safe_replace sub(m);
     // term -> var
-    sub.insert(term , var);
+    sub.insert(term, var);
     rational val;
     if (m_arith.is_numeral(term, val)) {
         bool is_int = val.is_int();
@@ -285,19 +339,17 @@ void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, var
 
     for (expr *lit : m_cube) {
         expr_ref abs_lit(m);
-        sub (lit,  abs_lit);
+        sub(lit, abs_lit);
-        if (lit == abs_lit) {
+        if (lit == abs_lit) {gnd_cube.push_back(lit);}
-            gnd_cube.push_back(lit);
-        }
         else {
             expr *e1, *e2;
             // generalize v=num into v>=num
             if (m.is_eq(abs_lit, e1, e2) && (e1 == var || e2 == var)) {
-            if (m_arith.is_numeral(e1)) {
+                if (m_arith.is_numeral(e1)) {
-                    abs_lit = m_arith.mk_ge (var, e1);
+                    abs_lit = m_arith.mk_ge(var, e1);
                 } else if (m_arith.is_numeral(e2)) {
                     abs_lit = m_arith.mk_ge(var, e2);
-            }
+                }
             }
             abs_cube.push_back(abs_lit);
             if (contains_selects(abs_lit, m)) {
@@ -454,9 +506,15 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
 
     mk_abs_cube(lemma, term, var, gnd_cube, abs_cube, lb, ub, stride);
     if (abs_cube.empty()) {return false;}
+    if (has_nlira(abs_cube)) {
+        TRACE("spacer_qgen",
+              tout << "non-linear expression: " << abs_cube << "\n";);
+        return false;
+    }
 
     TRACE("spacer_qgen",
           tout << "abs_cube is: " << mk_and(abs_cube) << "\n";
+          tout << "term: " << mk_pp(term, m) << "\n";
           tout << "lb = ";
           if (lb) tout << mk_pp(lb, m); else tout << "none";
           tout << "\n";
@@ -464,7 +522,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
           if (ub) tout << mk_pp(ub, m); else tout << "none";
           tout << "\n";);
 
-    if (!lb && !ub) 
+    if (!lb && !ub)
         return false;
 
     // -- guess lower or upper bound if missing
@@ -473,7 +531,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
         lb = abs_cube.back();
     }
     if (!ub) {
-        abs_cube.push_back (m_arith.mk_lt(var, term));
+        abs_cube.push_back (m_arith.mk_le(var, term));
         ub = abs_cube.back();
     }
 
@@ -489,10 +547,10 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
         TRACE("spacer_qgen",
               tout << "mod=" << mod << " init=" << init << " stride=" << stride << "\n";
               tout.flush(););
-        abs_cube.push_back(m.mk_eq(
+        abs_cube.push_back
-                m_arith.mk_mod(var, m_arith.mk_numeral(rational(stride), true)),
+            (m.mk_eq(m_arith.mk_mod(var,
-                m_arith.mk_numeral(rational(mod), true)));
+                                    m_arith.mk_numeral(rational(stride), true)),
-    }
+                     m_arith.mk_numeral(rational(mod), true)));}
 
     // skolemize
     expr_ref gnd(m);
@@ -512,21 +570,21 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
               << "New CUBE is: " << gnd_cube << "\n";);
         SASSERT(zks.size() >= static_cast<unsigned>(m_offset));
 
-                // lift quantified variables to top of select
+        // lift quantified variables to top of select
         expr_ref ext_bind(m);
         ext_bind = term;
         cleanup(gnd_cube, zks, ext_bind);
 
-                // XXX better do that check before changing bind in cleanup()
+        // XXX better do that check before changing bind in cleanup()
-                // XXX Or not because substitution might introduce _n variable into bind
+        // XXX Or not because substitution might introduce _n variable into bind
         if (m_ctx.get_manager().is_n_formula(ext_bind)) {
-                    // XXX this creates an instance, but not necessarily the needed one
+            // XXX this creates an instance, but not necessarily the needed one
 
-                    // XXX This is sound because any instance of
+            // XXX This is sound because any instance of
-                    // XXX universal quantifier is sound
+            // XXX universal quantifier is sound
 
-                    // XXX needs better long term solution. leave
+            // XXX needs better long term solution. leave
-                    // comment here for the future
+            // comment here for the future
             m_ctx.get_manager().formula_n2o(ext_bind, ext_bind, 0);
         }
 
@@ -542,46 +600,50 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
     return false;
 }
 
-bool lemma_quantifier_generalizer::find_stride(expr_ref_vector &c, expr_ref &pattern, unsigned &stride) {
+bool lemma_quantifier_generalizer::find_stride(expr_ref_vector &cube,
+                                               expr_ref &pattern,
+                                               unsigned &stride) {
     expr_ref tmp(m);
-    tmp = mk_and(c);
+    tmp = mk_and(cube);
     normalize(tmp, tmp, false, true);
-    c.reset();
+    cube.reset();
-    flatten_and(tmp, c);
+    flatten_and(tmp, cube);
 
     app_ref_vector indices(m);
-    get_select_indices(pattern, indices, m);
+    get_select_indices(pattern, indices);
 
-    // TODO
+    CTRACE("spacer_qgen", indices.empty(),
-    if (indices.size() > 1)
+           tout << "Found no select indices in: " << pattern << "\n";);
-        return false;
+
+    // TBD: handle multi-dimensional arrays and literals with multiple
+    // select terms
+    if (indices.size() != 1) return false;
 
     app *p_index = indices.get(0);
-    if (is_var(p_index)) return false;
 
-    std::vector<unsigned> instances;
+    unsigned_vector instances;
-    for (expr* lit : c) {
+    for (expr* lit : cube) {
 
         if (!contains_selects(lit, m))
             continue;
 
         indices.reset();
-        get_select_indices(lit, indices, m);
+        get_select_indices(lit, indices);
 
-        // TODO:
+        // TBD: handle multi-dimensional arrays
-        if (indices.size() > 1)
+        if (indices.size() != 1)
             continue;
 
         app *candidate = indices.get(0);
 
         unsigned size = p_index->get_num_args();
         unsigned matched = 0;
-        for (unsigned p=0; p < size; p++) {
+        for (unsigned p = 0; p < size; p++) {
             expr *arg = p_index->get_arg(p);
             if (is_var(arg)) {
                 rational val;
-                if (p < candidate->get_num_args() && 
+                if (p < candidate->get_num_args() &&
-                    m_arith.is_numeral(candidate->get_arg(p), val) && 
+                    m_arith.is_numeral(candidate->get_arg(p), val) &&
                     val.is_unsigned()) {
                     instances.push_back(val.get_unsigned());
                 }

src/muz/spacer/spacer_util.cpp

@@ -666,9 +666,6 @@ namespace {
             flatten_and(out, v);
 
             if (v.size() > 1) {
-                // sort arguments of the top-level and
-                std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
-
                 if (use_simplify_bounds) {
                     // remove redundant inequalities
                     simplify_bounds(v);
@@ -680,6 +677,8 @@ namespace {
                     v.reset();
                     egraph.to_lits(v);
                 }
+                // sort arguments of the top-level and
+                std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
 
                 TRACE("spacer_normalize",
                       tout << "Normalized:\n"
@@ -900,17 +899,22 @@ namespace {
     struct collect_indices {
         app_ref_vector& m_indices;
         array_util      a;
-        collect_indices(app_ref_vector& indices): m_indices(indices), a(indices.get_manager()) {}
+        collect_indices(app_ref_vector& indices): m_indices(indices),
+                                                  a(indices.get_manager()) {}
         void operator()(expr* n) {}
         void operator()(app* n) {
-            if (a.is_select(n))
+            if (a.is_select(n)) {
-                for (unsigned i = 1; i < n->get_num_args(); ++i)
+                // for all but first argument
-                    if (is_app(n->get_arg(i)))
+                for (unsigned i = 1; i < n->get_num_args(); ++i) {
-                        m_indices.push_back(to_app(n->get_arg(i)));
+                    expr *arg = n->get_arg(i);
+                    if (is_app(arg))
+                        m_indices.push_back(to_app(arg));
+                }
+            }
         }
     };
 
-    void get_select_indices(expr* fml, app_ref_vector &indices, ast_manager& m) {
+    void get_select_indices(expr* fml, app_ref_vector &indices) {
         collect_indices ci(indices);
         for_each_expr(ci, fml);
     }

src/muz/spacer/spacer_util.h

@@ -121,7 +121,7 @@ namespace spacer {
     void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml);
 
     bool contains_selects (expr* fml, ast_manager& m);
-    void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m);
+    void get_select_indices (expr* fml, app_ref_vector& indices);
 
     void find_decls (expr* fml, app_ref_vector& decls, std::string& prefix);
 

src/qe/qe_lite.cpp

@@ -320,8 +320,8 @@ namespace eq {
                        << "sz is " << sz << "\n"
                        << "subst_map[inx]: " << mk_pp(m_subst_map.get(inx), m) << "\n";);
                 SASSERT(m_subst_map.get(inx) == nullptr);
-                m_subst_map[inx] = r;
                 m_subst.update_inv_binding_at(inx, r);
+                m_subst_map[inx] = std::move(r);
             }
         }
 
@@ -470,7 +470,7 @@ namespace eq {
                             m_var2pos[idx] = i;
                             def_count++;
                             largest_vinx = std::max(idx, largest_vinx);
-                            m_new_exprs.push_back(t);
+                            m_new_exprs.push_back(std::move(t));
                         }
                         else if (!m.is_value(m_map[idx])) {
                             // check if the new definition is simpler
@@ -482,7 +482,7 @@ namespace eq {
                                 m_pos2var[i] = idx;
                                 m_var2pos[idx] = i;
                                 m_map[idx] = t;
-                                m_new_exprs.push_back(t);
+                                m_new_exprs.push_back(std::move(t));
                           }
                           // -- prefer ground
                           else if (is_app(t) && to_app(t)->is_ground() &&
@@ -492,7 +492,7 @@ namespace eq {
                               m_pos2var[i] = idx;
                               m_var2pos[idx] = i;
                               m_map[idx] = t;
-                              m_new_exprs.push_back(t);
+                              m_new_exprs.push_back(std::move(t));
                           }
                           // -- prefer constants
                           else if (is_uninterp_const(t)
@@ -501,7 +501,7 @@ namespace eq {
                               m_pos2var[i] = idx;
                               m_var2pos[idx] = i;
                               m_map[idx] = t;
-                              m_new_exprs.push_back(t);
+                              m_new_exprs.push_back(std::move(t));
                           }
                           TRACE ("qe_def",
                                  tout << "Replacing definition of VAR " << idx << " from "

src/qe/qe_term_graph.cpp

@@ -200,7 +200,8 @@ namespace qe {
         }
 
         std::ostream& display(std::ostream& out) const {
-            out << get_id() << ": " << m_expr << " - ";
+            out << get_id() << ": " << m_expr 
+                << (is_root() ? " R" : "") << " - ";
             term const* r = &this->get_next();
             while (r != this) {
                 out << r->get_id() << " ";
@@ -371,20 +372,20 @@ namespace qe {
     }
 
     void term_graph::merge(term &t1, term &t2) {
-        // -- merge might invalidate term2app cache
-        m_term2app.reset();
-        m_pinned.reset();
-
         term *a = &t1.get_root();
         term *b = &t2.get_root();
 
         if (a == b) return;
 
+        // -- merge might invalidate term2app cache
+        m_term2app.reset();
+        m_pinned.reset();
+
         if (a->get_class_size() > b->get_class_size()) {
             std::swap(a, b);
         }
 
-        // Remove parents of it from the cg table.
+        // Remove parents of b from the cg table.
         for (term* p : term::parents(b)) {
             if (!p->is_marked()) {
                 p->set_mark(true);
@@ -401,7 +402,7 @@ namespace qe {
         a->merge_eq_class(*b);
 
         // Insert parents of b's old equilvalence class into the cg table
-        for (term* p : term::parents(a)) {
+        for (term* p : term::parents(b)) {
             if (p->is_marked()) {
                 term* p_old = m_cg_table.insert_if_not_there(p);
                 p->set_mark(false);
@@ -412,6 +413,7 @@ namespace qe {
                 }
             }
         }
+        SASSERT(marks_are_clear());
     }
 
     expr* term_graph::mk_app_core (expr *e) {
@@ -484,10 +486,16 @@ namespace qe {
         }
     }
 
+    bool term_graph::marks_are_clear() {
+        for (term * t : m_terms) {
+            if (t->is_marked()) return false;
+        }
+        return true;
+    }
+
     /// Order of preference for roots of equivalence classes
     /// XXX This should be factored out to let clients control the preference
     bool term_graph::term_lt(term const &t1, term const &t2) {
-
         // prefer constants over applications
         // prefer uninterpreted constants over values
         // prefer smaller expressions over larger ones
@@ -521,6 +529,7 @@ namespace qe {
 
     /// Choose better roots for equivalence classes
     void term_graph::pick_roots() {
+        SASSERT(marks_are_clear());
         for (term* t : m_terms) {
             if (!t->is_marked() && t->is_root())
                 pick_root(*t);
@@ -589,7 +598,7 @@ namespace qe {
                 // prefer a node that resembles current child, 
                 // otherwise, pick a root representative, if present.
                 if (m_term2app.find(ch->get_id(), e))
-                    kids.push_back(e);
+                kids.push_back(e);
                 else if (m_root2rep.find(ch->get_root().get_id(), e)) 
                     kids.push_back(e);
                 else 

src/qe/qe_term_graph.h

@@ -75,6 +75,7 @@ namespace qe {
         void pick_roots();
 
         void reset_marks();
+        bool marks_are_clear();
 
         expr* mk_app_core(expr* a);
         expr_ref mk_app(term const &t);

src/smt/mam.cpp

@@ -2000,7 +2000,8 @@ namespace smt {
             if (t->filter_candidates()) {
                 for (enode* app : t->get_candidates()) {
                     if (!app->is_marked() && app->is_cgr()) {
-                        execute_core(t, app);
+                        if (m_context.resource_limits_exceeded() || !execute_core(t, app))
+                            return;
                         app->set_mark();
                     }
                 }
@@ -2014,14 +2015,15 @@ namespace smt {
                     TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
                     if (app->is_cgr()) {
                         TRACE("trigger_bug", tout << "is_cgr\n";);
-                        execute_core(t, app);
+                        if (m_context.resource_limits_exceeded() || !execute_core(t, app))
+                            return;
                     }
                 }
             }
         }
 
         // init(t) must be invoked before execute_core
-        void execute_core(code_tree * t, enode * n);
+        bool execute_core(code_tree * t, enode * n);
 
         // Return the min, max generation of the enodes in m_pattern_instances.
 
@@ -2250,7 +2252,7 @@ namespace smt {
         display_instr_input_reg(out, m_pc);
     }
 
-    void interpreter::execute_core(code_tree * t, enode * n) {
+    bool interpreter::execute_core(code_tree * t, enode * n) {
         TRACE("trigger_bug", tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode\n" << mk_ismt2_pp(n->get_owner(), m_ast_manager) << "\n";);
         unsigned since_last_check = 0;
 
@@ -2494,7 +2496,7 @@ namespace smt {
 #define ON_MATCH(NUM)                                                   \
             m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \
             if (m_context.get_cancel_flag()) {                          \
-                return;                                                 \
+                return false;                                           \
             }                                                           \
             m_mam.on_match(static_cast<const yield *>(m_pc)->m_qa,                                      \
                            static_cast<const yield *>(m_pc)->m_pat,                                     \
@@ -2647,7 +2649,7 @@ namespace smt {
 #ifdef _PROFILE_MAM
             t->get_watch().stop();
 #endif
-            return; // no more alternatives
+            return true; // no more alternatives
         }
         backtrack_point & bp = m_backtrack_stack[m_top - 1];
         m_max_generation     = bp.m_old_max_generation;
@@ -2675,7 +2677,7 @@ namespace smt {
 #ifdef _PROFILE_MAM
                t->get_watch().stop();
 #endif
-                return;
+                return false;
             }
         }
 

src/smt/smt_context.cpp

@@ -1594,7 +1594,7 @@ namespace smt {
         for (literal lit : m_assigned_literals) {
             expr_ref e(m_manager);
             literal2expr(lit, e);
-            assignments.push_back(e);
+            assignments.push_back(std::move(e));
         }
     }
 
@@ -4180,7 +4180,7 @@ namespace smt {
             SASSERT(get_justification(guess.var()).get_kind() == b_justification::AXIOM);
             expr_ref lit(m_manager);
             literal2expr(guess, lit);
-            result.push_back(lit);
+            result.push_back(std::move(lit));
         }
     }
 

src/smt/smt_context.h

@@ -1115,8 +1115,6 @@ namespace smt {
 
         void internalize_assertions();
 
-        void assert_assumption(expr * a);
-
         bool validate_assumptions(expr_ref_vector const& asms);
 
         void init_assumptions(expr_ref_vector const& asms);
@@ -1129,8 +1127,6 @@ namespace smt {
 
         void reset_assumptions();
 
-        void reset_clause();
-
         void add_theory_assumptions(expr_ref_vector & theory_assumptions);
 
         lbool mk_unsat_core(lbool result);
@@ -1585,8 +1581,6 @@ namespace smt {
 
         //proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); }
 
-        void get_assumptions_core(ptr_vector<expr> & result);
-
         void get_assertions(ptr_vector<expr> & result) { m_asserted_formulas.get_assertions(result); }
 
         void display(std::ostream & out) const;

src/smt/smt_context_pp.cpp

@@ -409,11 +409,11 @@ namespace smt {
         for (unsigned i = 0; i < num_antecedents; i++) {
             literal l = antecedents[i];
             literal2expr(l, n);
-            fmls.push_back(n);
+            fmls.push_back(std::move(n));
         }
         if (consequent != false_literal) {
             literal2expr(~consequent, n);
-            fmls.push_back(n);
+            fmls.push_back(std::move(n));
         }
         if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
         visitor.collect(fmls);

src/smt/smt_justification.cpp

@@ -281,7 +281,7 @@ namespace smt {
         for (unsigned i = 0; i < m_num_literals; i++) {
             expr_ref l(m);
             ctx.literal2expr(m_literals[i], l);
-            lits.push_back(l);
+            lits.push_back(std::move(l));
         }
         if (lits.size() == 1)
             return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr());
@@ -407,12 +407,7 @@ namespace smt {
         for (unsigned i = 0; i < m_num_literals; i++) {
             bool sign   = GET_TAG(m_literals[i]) != 0;
             expr * v    = UNTAG(expr*, m_literals[i]);
-            expr_ref l(m);
+            lits.push_back(sign ? m.mk_not(v) : v);
-            if (sign) 
-                l       = m.mk_not(v);
-            else
-                l       = v;
-            lits.push_back(l);
         }
         if (lits.size() == 1)
             return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr());

src/solver/solver_pool.cpp

@@ -101,9 +101,11 @@ public:
     proof * get_proof() override {
         scoped_watch _t_(m_pool.m_proof_watch);
         if (!m_proof.get()) {
-            elim_aux_assertions pc(m_pred);
             m_proof = m_base->get_proof();
-            pc(m, m_proof, m_proof);
+            if (m_proof) {
+                elim_aux_assertions pc(m_pred);
+                pc(m, m_proof, m_proof);
+            }
         }
         return m_proof;
     }

src/tactic/smtlogics/qfufbv_tactic.cpp

@@ -62,7 +62,7 @@ public:
 
         TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
         // running implementation
-        expr_ref_vector flas(m);
+        ptr_vector<expr> flas;
         const unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
         scoped_ptr<solver> uffree_solver = setup_sat();

src/util/ref_vector.h

@@ -99,6 +99,13 @@ public:
         return *this;
     }
 
+    template <typename W, typename M>
+    ref_vector_core& push_back(obj_ref<W,M> && n) {
+        m_nodes.push_back(n.get());
+        n.steal();
+        return *this;
+    }
+
     void pop_back() {
         SASSERT(!m_nodes.empty());
         T * n = m_nodes.back();
@@ -253,6 +260,13 @@ public:
             return *this;
         }
 
+        template <typename W, typename M>
+        element_ref & operator=(obj_ref<W,M> && n) {
+            m_manager.dec_ref(m_ref);
+            m_ref = n.steal();
+            return *this;
+        }
+
         T * get() const {
             return m_ref;
         }
@@ -288,9 +302,8 @@ public:
         return *this;
     }
     
-private:
     // prevent abuse:
-    ref_vector & operator=(ref_vector const & other);
+    ref_vector & operator=(ref_vector const & other) = delete;
 };
 
 template<typename T>