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

scripts/mk_util.py

@@ -461,7 +461,6 @@ def check_dotnet_core():
     r = exec_cmd([DOTNET, '--help'])
     if r != 0:
         raise MKException('Failed testing dotnet. Make sure to install and configure dotnet core utilities')
-    pass
 
 def check_ml():
     t = TempFile('hello.ml')

scripts/mk_win_dist.py

@@ -25,6 +25,7 @@ VERBOSE=True
 DIST_DIR='dist'
 FORCE_MK=False
 DOTNET_ENABLED=True
+DOTNET_CORE_ENABLED=False
 DOTNET_KEY_FILE=None
 JAVA_ENABLED=True
 GIT_HASH=False
@@ -62,6 +63,7 @@ def display_help():
     print("  -b <sudir>, --build=<subdir>  subdirectory where x86 and x64 Z3 versions will be built (default: build-dist).")
     print("  -f, --force                   force script to regenerate Makefiles.")
     print("  --nodotnet                    do not include .NET bindings in the binary distribution files.")
+    print("  --dotnetcore                  build for dotnet core.")
     print("  --dotnet-key=<file>           sign the .NET assembly with the private key in <file>.")
     print("  --nojava                      do not include Java bindings in the binary distribution files.")
     print("  --nopython                    do not include Python bindings in the binary distribution files.")
@@ -72,7 +74,7 @@ def display_help():
 
 # Parse configuration option for mk_make script
 def parse_options():
-    global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, X86ONLY, X64ONLY
+    global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, X86ONLY, X64ONLY
     path = BUILD_DIR
     options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
                                                                    'help',
@@ -80,6 +82,7 @@ def parse_options():
                                                                    'force',
                                                                    'nojava',
                                                                    'nodotnet',
+                                                                   'dotnetcore',
                                                                    'dotnet-key=',
                                                                    'githash',
                                                                    'nopython',
@@ -99,6 +102,8 @@ def parse_options():
             FORCE_MK = True
         elif opt == '--nodotnet':
             DOTNET_ENABLED = False
+        elif opt == '--dotnetcore':
+            DOTNET_CORE_ENABLED = True
         elif opt == '--nopython':
             PYTHON_ENABLED = False
         elif opt == '--dotnet-key':
@@ -124,7 +129,11 @@ def mk_build_dir(path, x64):
     if not check_build_dir(path) or FORCE_MK:
         parallel = '--parallel=' + MAKEJOBS
         opts = ["python", os.path.join('scripts', 'mk_make.py'), parallel, "-b", path]
-        if DOTNET_ENABLED:
+        if DOTNET_CORE_ENABLED:
+            opts.append('--dotnetcore')
+            if not DOTNET_KEY_FILE is None:
+                opts.append('--dotnet-key=' + DOTNET_KEY_FILE)
+        elif DOTNET_ENABLED:
             opts.append('--dotnet')
             if not DOTNET_KEY_FILE is None:
                 opts.append('--dotnet-key=' + DOTNET_KEY_FILE)
@@ -208,7 +217,10 @@ def mk_dist_dir(x64):
         build_path = BUILD_X86_DIR
     dist_path = os.path.join(DIST_DIR, get_z3_name(x64))
     mk_dir(dist_path)
-    mk_util.DOTNET_CORE_ENABLED = DOTNET_ENABLED
+    if DOTNET_CORE_ENABLED:
+       mk_util.DOTNET_CORE_ENABLED = True
+    else:
+       mk_util.DOTNET_ENABLED = DOTNET_ENABLED
     mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE
     mk_util.JAVA_ENABLED = JAVA_ENABLED
     mk_util.PYTHON_ENABLED = PYTHON_ENABLED

src/api/dotnet/Context.cs

@@ -931,6 +931,26 @@ namespace Microsoft.Z3
             return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject));
         }
 
+        /// <summary>
+        /// Create an expression representing <c>t1 xor t2 xor t3 ... </c>.
+        /// </summary>
+        public BoolExpr MkXor(IEnumerable<BoolExpr> ts)
+        {
+            Debug.Assert(ts != null);
+            Debug.Assert(ts.All(a => a != null));
+            CheckContextMatch<BoolExpr>(ts);
+            BoolExpr r = null;
+            foreach (var t in ts) {
+                if (r == null) 
+                   r = t;
+                else
+                   r = MkXor(r, t);
+            }
+            if (r == null) 
+               r = MkTrue();
+            return r;
+        }
+
         /// <summary>
         /// Create an expression representing <c>t[0] and t[1] and ...</c>.
         /// </summary>

src/api/dotnet/Model.cs

@@ -238,6 +238,14 @@ namespace Microsoft.Z3
             return Eval(t, completion);
         }
 
+        /// <summary>
+        /// Evaluate expression to a double, assuming it is a numeral already.
+        /// </summary>
+        public double Double(Expr t) {
+            var r = Eval(t, true);
+            return Native.Z3_get_numeral_double(Context.nCtx, r.NativeObject);
+        }
+
         /// <summary>
         /// The number of uninterpreted sorts that the model has an interpretation for.
         /// </summary>    

src/api/java/Context.java

@@ -2173,6 +2173,22 @@ public class Context implements AutoCloseable {
     {
         checkContextMatch(t);
         return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t)));
+    }
+
+    /**
+     * Create the empty regular expression.
+     */
+    public ReExpr mkEmptyRe(Sort s) 
+    {
+	return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject()));
+    }
+
+    /**
+     * Create the full regular expression.
+     */
+    public ReExpr mkFullRe(Sort s) 
+    {
+	return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject()));
     }    
     
     /**

src/api/python/z3/z3.py

@@ -6164,6 +6164,10 @@ class ModelRef(Z3PPObject):
     def __deepcopy__(self):
         return self.translate(self.ctx)
 
+def Model(ctx = None):
+    ctx = _get_ctx(ctx)
+    return ModelRef(Z3_mk_model(ctx.ref()), ctx)
+
 def is_as_array(n):
     """Return true if n is a Z3 expression of the form (_ as-array f)."""
     return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())

src/api/z3_api.h

@@ -5579,7 +5579,7 @@ extern "C" {
        \brief Convert a goal into a DIMACS formatted string.
        The goal must be in CNF. You can convert a goal to CNF
        by applying the tseitin-cnf tactic. Bit-vectors are not automatically
-       converted to Booleans either, so the caller intends to 
+       converted to Booleans either, so if the caller intends to
        preserve satisfiability, it should apply bit-blasting tactics.
        Quantifiers and theory atoms will not be encoded.
 

src/opt/maxres.cpp

@@ -108,6 +108,7 @@ private:
     bool             m_pivot_on_cs;            // prefer smaller correction set to core.
     bool             m_dump_benchmarks;        // display benchmarks (into wcnf format)
 
+    
 
     std::string      m_trace_id;
     typedef ptr_vector<expr> exprs;
@@ -152,6 +153,14 @@ public:
             (m.is_not(l, l) && is_uninterp_const(l));
     }    
 
+    void add(expr_ref_vector const& es) {
+        for (expr* e : es) add(e);
+    }
+
+    void add(expr* e) {
+        s().assert_expr(e);
+    }
+
     void add_soft(expr* e, rational const& w) {
         TRACE("opt", tout << mk_pp(e, m) << " |-> " << w << "\n";);
         expr_ref asum(m), fml(m);
@@ -168,7 +177,7 @@ public:
         else {
             asum = mk_fresh_bool("soft");
             fml = m.mk_iff(asum, e);
-            s().assert_expr(fml);
+            add(fml);
         }
         new_assumption(asum, w);
     }
@@ -194,11 +203,8 @@ public:
         if (is_sat != l_true) return is_sat;
         while (m_lower < m_upper) {
             TRACE("opt_verbose", 
-                  display_vec(tout, m_asms);
+                  s().display(tout << m_asms << "\n") << "\n";
-                  s().display(tout);
+                  display(tout););
-                  tout << "\n";
-                  display(tout);
-                  );
             is_sat = check_sat_hill_climb(m_asms);
             if (m.canceled()) {
                 return l_undef;
@@ -206,8 +212,7 @@ public:
             switch (is_sat) {
             case l_true: 
                 CTRACE("opt", !m_model->is_true(m_asms), 
-                       tout << *m_model;
+                       tout << *m_model << "assumptions: ";
-                       tout << "assumptions: ";
                        for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " ";
                        tout << "\n";);
                 SASSERT(m_model->is_true(m_asms));
@@ -320,6 +325,7 @@ public:
 
     void found_optimum() {
         IF_VERBOSE(1, verbose_stream() << "found optimum\n";);
+        verify_assumptions();
         m_lower.reset();
         for (soft& s : m_soft) {
             s.is_true = m_model->is_true(s.s);
@@ -348,7 +354,14 @@ public:
         st.update("maxres-correction-sets", m_stats.m_num_cs);
     }
 
-    lbool get_cores(vector<exprs>& cores) {
+    struct weighted_core {
+        exprs    m_core;
+        rational m_weight;
+        weighted_core(exprs const& c, rational const& w):
+            m_core(c), m_weight(w) {}
+    };
+
+    lbool get_cores(vector<weighted_core>& cores) {
         // assume m_s is unsat.
         lbool is_sat = l_false;
         cores.reset();
@@ -361,7 +374,7 @@ public:
             get_mus_model(mdl);
             is_sat = minimize_core(_core);
             core.append(_core.size(), _core.c_ptr());
-            // verify_core(core);
+            verify_core(core);
             ++m_stats.m_num_cores;
             if (is_sat != l_true) {
                 IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";);
@@ -373,13 +386,16 @@ public:
                 m_lower = m_upper;
                 return l_true;
             }
+
+            
             // 1. remove all core literals from m_asms
             // 2. re-add literals of higher weight than min-weight.
             // 3. 'core' stores the core literals that are
             //    re-encoded as assumptions, afterwards
+            cores.push_back(weighted_core(core, core_weight(core)));
+
             remove_soft(core, m_asms);
-            split_core(core);
+            split_core(core);  
-            cores.push_back(core);
 
             if (core.size()  >= m_max_core_size) break;
             if (cores.size() >= m_max_num_cores) break;
@@ -389,7 +405,7 @@ public:
 
         TRACE("opt", 
               tout << "sat: " << is_sat << " num cores: " << cores.size() << "\n";
-              for (auto const& c : cores) display_vec(tout, c);
+              for (auto const& c : cores) display_vec(tout, c.m_core);
               tout << "num assumptions: " << m_asms.size() << "\n";);
         
         return is_sat;
@@ -456,7 +472,7 @@ public:
     }
 
     lbool process_unsat() {
-        vector<exprs> cores;
+        vector<weighted_core> cores;
         lbool is_sat = get_cores(cores);
         if (is_sat != l_true) {
             return is_sat;
@@ -478,9 +494,9 @@ public:
         return result;
     }
 
-    void process_unsat(vector<exprs> const& cores) {
+    void process_unsat(vector<weighted_core> const& cores) {
         for (auto const & c : cores) {
-            process_unsat(c);
+            process_unsat(c.m_core, c.m_weight);
         }
     }
 
@@ -491,16 +507,15 @@ public:
         }
     }
     
-    void process_unsat(exprs const& core) {
+    void process_unsat(exprs const& core, rational w) {
         IF_VERBOSE(3, verbose_stream() << "(maxres cs model valid: " << (m_csmodel.get() != nullptr) << " cs size:" << m_correction_set_size << " core: " << core.size() << ")\n";);
         expr_ref fml(m);
         SASSERT(!core.empty());
-        rational w = core_weight(core);
         TRACE("opt", display_vec(tout << "minimized core: ", core););
-        IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core););
+        IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core););        
         max_resolve(core, w);
         fml = mk_not(m, mk_and(m, core.size(), core.c_ptr()));
-        s().assert_expr(fml);
+        add(fml);
         m_lower += w;
         if (m_st == s_primal_dual) {
             m_lower = std::min(m_lower, m_upper);
@@ -636,10 +651,10 @@ public:
             else {
                 dd = mk_fresh_bool("d");
                 fml = m.mk_implies(dd, d);
-                s().assert_expr(fml);
+                add(fml);
                 m_defs.push_back(fml);
                 fml = m.mk_implies(dd, b_i);
-                s().assert_expr(fml);
+                add(fml);
                 m_defs.push_back(fml);
                 fml = m.mk_and(d, b_i);
                 update_model(dd, fml);
@@ -650,7 +665,7 @@ public:
             fml = m.mk_implies(asum, cls);
             update_model(asum, cls);
             new_assumption(asum, w);
-            s().assert_expr(fml);
+            add(fml);
             m_defs.push_back(fml);
         }
     }
@@ -682,7 +697,7 @@ public:
                 d = mk_fresh_bool("d");
                 fml = m.mk_implies(d, cls);
                 update_model(d, cls);
-                s().assert_expr(fml);
+                add(fml);
                 m_defs.push_back(fml);
                 
             }
@@ -691,10 +706,10 @@ public:
             }
             asum = mk_fresh_bool("a");
             fml = m.mk_implies(asum, b_i1);
-            s().assert_expr(fml);
+            add(fml);
             m_defs.push_back(fml);
             fml = m.mk_implies(asum, cls);
-            s().assert_expr(fml);
+            add(fml);
             m_defs.push_back(fml);
             new_assumption(asum, w);
 
@@ -702,7 +717,7 @@ public:
             update_model(asum, fml);
         }
         fml = m.mk_or(cs.size(), cs.c_ptr());
-        s().assert_expr(fml);
+        add(fml);
     }
 
     void update_assignment(model_ref & mdl) {
@@ -747,7 +762,7 @@ public:
             s.is_true = m_model->is_true(s.s);
         }
        
-        // DEBUG_CODE(verify_assignment(););
+        verify_assignment();
 
         m_upper = upper;
         
@@ -768,7 +783,7 @@ public:
         }            
         fml = u.mk_lt(nsoft.size(), weights.c_ptr(), nsoft.c_ptr(), m_upper);
         TRACE("opt", tout << "block upper bound " << fml << "\n";);;
-        s().assert_expr(fml); 
+        add(fml); 
     }
 
     void remove_soft(exprs const& core, expr_ref_vector& asms) {
@@ -819,40 +834,50 @@ public:
     void commit_assignment() override {
         if (m_found_feasible_optimum) {
             TRACE("opt", tout << "Committing feasible solution\n" << m_defs << " " << m_asms;);
-            s().assert_expr(m_defs);
+            add(m_defs);
-            s().assert_expr(m_asms);
+            add(m_asms);
         }
         // else: there is only a single assignment to these soft constraints.
     }
 
     void verify_core(exprs const& core) {
-        IF_VERBOSE(3, verbose_stream() << "verify core\n";);                
+        return;
-        ref<solver> smt_solver = mk_smt_solver(m, m_params, symbol());
+        IF_VERBOSE(3, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";);                
-        smt_solver->assert_expr(s().get_assertions());
+        ref<solver> _solver = mk_smt_solver(m, m_params, symbol());
-        smt_solver->assert_expr(core);
+        _solver->assert_expr(s().get_assertions());
-        lbool is_sat = smt_solver->check_sat(0, nullptr);
+        _solver->assert_expr(core);
-        if (is_sat == l_true) {
+        lbool is_sat = _solver->check_sat(0, nullptr);
-            IF_VERBOSE(0, verbose_stream() << "not a core\n";);
+        IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << "\n");
-        }        
+        VERIFY(is_sat == l_false);
+    }
+
+    void verify_assumptions() {
+        return;
+        IF_VERBOSE(1, verbose_stream() << "verify assumptions\n";);        
+        ref<solver> _solver = mk_smt_solver(m, m_params, symbol());
+        _solver->assert_expr(s().get_assertions());
+        _solver->assert_expr(m_asms);
+        lbool is_sat = _solver->check_sat(0, nullptr);
+        IF_VERBOSE(1, verbose_stream() << "assignment status (l_true) " << is_sat << "\n";);               
+        VERIFY(is_sat == l_true);
     }
 
     void verify_assignment() {
+        return;
         IF_VERBOSE(1, verbose_stream() << "verify assignment\n";);        
-        ref<solver> smt_solver = mk_smt_solver(m, m_params, symbol());
+        ref<solver> _solver = mk_smt_solver(m, m_params, symbol());
-        smt_solver->assert_expr(s().get_assertions());
+        _solver->assert_expr(s().get_assertions());
         expr_ref n(m);
         for (soft& s : m_soft) {
             n = s.s;
             if (!s.is_true) {
                 n = mk_not(m, n);
             }
-            smt_solver->assert_expr(n);
+            _solver->assert_expr(n);
         }
-        lbool is_sat = smt_solver->check_sat(0, nullptr);
+        lbool is_sat = _solver->check_sat(0, nullptr);
-        if (is_sat == l_false) {
+        IF_VERBOSE(1, verbose_stream() << "assignment status (l_true) " << is_sat << "\n");
-            IF_VERBOSE(0, verbose_stream() << "assignment is infeasible\n";);
+        VERIFY(is_sat == l_true);
-        }
-        IF_VERBOSE(1, verbose_stream() << "verified\n";);        
     }
 };
 

src/opt/opt_context.cpp

@@ -284,7 +284,9 @@ namespace opt {
         symbol pri = optp.priority();
 
         IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n");
+        
         lbool is_sat = s.check_sat(asms.size(),asms.c_ptr());
+
         TRACE("opt", s.display(tout << "initial search result: " << is_sat << "\n");); 
         if (is_sat != l_false) {
             s.get_model(m_model);
@@ -1565,11 +1567,12 @@ namespace opt {
         mdl->set_model_completion(true);
         for (expr * f : fmls) {
             if (!mdl->is_true(f)) {
-                //IF_VERBOSE(0, m_fm->display(verbose_stream() << "fm\n"));
+                IF_VERBOSE(0, 
-                IF_VERBOSE(0, m_model_converter->display(verbose_stream() << "mc\n"));
+                           verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n";
-                IF_VERBOSE(0, verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n");
+                           m_fm->display(verbose_stream() << "fm\n");
-                IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *mdl, 0)); 
+                           m_model_converter->display(verbose_stream() << "mc\n");
-                IF_VERBOSE(11, verbose_stream() << to_string_internal() << "\n");
+                           model_smt2_pp(verbose_stream(), m, *mdl, 0);
+                           verbose_stream() << to_string_internal() << "\n");
                 exit(0);
             }
         }

src/smt/theory_arith_core.h

@@ -503,7 +503,7 @@ namespace smt {
                   tout << "lower: " << lower << "\n";
                   tout << "upper: " << upper << "\n";);
 
-            mk_axiom(eqz, eq,    true);
+            mk_axiom(eqz, eq,    false);
             mk_axiom(eqz, lower, false);
             mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
             rational k;

src/solver/check_sat_result.cpp

@@ -36,6 +36,7 @@ void check_sat_result::set_reason_unknown(event_handler& eh) {
     }
 }
 
+
 simple_check_sat_result::simple_check_sat_result(ast_manager & m):
     m_core(m),
     m_proof(m) {

src/solver/solver.h

@@ -146,6 +146,8 @@ public:
     
     lbool check_sat(app_ref_vector const& asms) { return check_sat(asms.size(), (expr* const*)asms.c_ptr()); }
 
+    lbool check_sat() { return check_sat(0, nullptr); }
+
     /**
        \brief Check satisfiability modulo a cube and a clause.
 

src/tactic/bv/bit_blaster_model_converter.cpp

@@ -72,10 +72,8 @@ struct bit_blaster_model_converter : public model_converter {
         }
         TRACE("blaster_mc",
               tout << "bits that should not be included in the model:\n";
-              obj_hashtable<func_decl>::iterator it  = bits.begin();
+              for (func_decl* f : bits) {
-              obj_hashtable<func_decl>::iterator end = bits.end();
+                  tout << f->get_name() << " ";
-              for (; it != end; ++it) {
-                  tout << (*it)->get_name() << " ";
               }
               tout << "\n";);
 

src/util/gparams.cpp

@@ -520,7 +520,7 @@ public:
             try {
                 symbol m, p;
                 normalize(name, m, p);
-                std::cout << name << " " << m << " " << p << "\n";
+                out << name << " " << m << " " << p << "\n";
                 param_descrs * d;
                 if (m == symbol::null) {
                     d = &get_param_descrs();

src/util/params.cpp

@@ -161,19 +161,15 @@ struct param_descrs::imp {
 
     void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
         svector<symbol> names;
-        dictionary<info>::iterator it  = m_info.begin();
+        for (auto const& kv : m_info) {
-        dictionary<info>::iterator end = m_info.end();
+            names.push_back(kv.m_key);
-        for (; it != end; ++it) {
-            names.push_back(it->m_key);
         }
         std::sort(names.begin(), names.end(), lt());
-        svector<symbol>::iterator it2  = names.begin();
+        for (symbol const& name : names) {
-        svector<symbol>::iterator end2 = names.end();
-        for (; it2 != end2; ++it2) {
             for (unsigned i = 0; i < indent; i++) out << " ";
             if (smt2_style)
                 out << ':';
-            char const * s = it2->bare_str();
+            char const * s = name.bare_str();
             unsigned n = static_cast<unsigned>(strlen(s));
             for (unsigned i = 0; i < n; i++) {
                 if (smt2_style && s[i] == '_')
@@ -186,7 +182,7 @@ struct param_descrs::imp {
                     out << s[i];
             }
             info d;
-            m_info.find(*it2, d);
+            m_info.find(name, d);
             SASSERT(d.m_descr);
             out << " (" << d.m_kind << ")";
             if (include_descr)
@@ -198,10 +194,8 @@ struct param_descrs::imp {
     }
 
     void copy(param_descrs & other) {
-        dictionary<info>::iterator it  = other.m_imp->m_info.begin();
+        for (auto const& kv : other.m_imp->m_info) {
-        dictionary<info>::iterator end = other.m_imp->m_info.end();
+            insert(kv.m_key, kv.m_value.m_kind, kv.m_value.m_descr, kv.m_value.m_default, kv.m_value.m_module);
-        for (; it != end; ++it) {
-            insert(it->m_key, it->m_value.m_kind, it->m_value.m_descr, it->m_value.m_default, it->m_value.m_module);
         }
     }
 
@@ -346,24 +340,22 @@ public:
     void reset(symbol const & k);
     void reset(char const * k);
 
-    void validate(param_descrs const & p) {
+    void validate(param_descrs const & p) {        
-        svector<params::entry>::iterator it  = m_entries.begin();  
-        svector<params::entry>::iterator end = m_entries.end();
         symbol suffix, prefix;
-        for (; it != end; ++it) {                                
+        for (params::entry& e : m_entries) {
-            param_kind expected = p.get_kind_in_module(it->first);
+            param_kind expected = p.get_kind_in_module(e.first);
             if (expected == CPK_INVALID) {
                 std::stringstream strm;
-                strm << "unknown parameter '" << it->first.str() << "'\n";    
+                strm << "unknown parameter '" << e.first.str() << "'\n";    
                 strm << "Legal parameters are:\n";
                 p.display(strm, 2, false, false);
                 throw default_exception(strm.str());
             }
-            if (it->second.m_kind != expected && 
+            if (e.second.m_kind != expected && 
-                !(it->second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) {
+                !(e.second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) {
                 std::stringstream strm;
-                strm << "Parameter " << it->first.str() << " was given argument of type ";
+                strm << "Parameter " << e.first.str() << " was given argument of type ";
-                strm << it->second.m_kind << ", expected " << expected;                
+                strm << e.second.m_kind << ", expected " << expected;                
                 throw default_exception(strm.str());
             }
         }
@@ -405,28 +397,26 @@ public:
 
     void display(std::ostream & out) const {
         out << "(params";
-        svector<params::entry>::const_iterator it  = m_entries.begin();  
+        for (params::entry const& e : m_entries) {
-        svector<params::entry>::const_iterator end = m_entries.end();
+            out << " " << e.first;            
-        for (; it != end; ++it) {
+            switch (e.second.m_kind) {
-            out << " " << it->first;            
-            switch (it->second.m_kind) {
             case CPK_BOOL:
-                out << " " << (it->second.m_bool_value?"true":"false");
+                out << " " << (e.second.m_bool_value?"true":"false");
                 break;
             case CPK_UINT:
-                out << " " <<it->second.m_uint_value;
+                out << " " <<e.second.m_uint_value;
                 break;
             case CPK_DOUBLE:
-                out << " " << it->second.m_double_value;
+                out << " " << e.second.m_double_value;
                 break;
             case CPK_NUMERAL:
-                out << " " << *(it->second.m_rat_value);
+                out << " " << *(e.second.m_rat_value);
                 break;
             case CPK_SYMBOL:
-                out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);
+                out << " " << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value);
                 break;
             case CPK_STRING:
-                out << " " << it->second.m_str_value;
+                out << " " << e.second.m_str_value;
                 break;
             default:
                 UNREACHABLE();
@@ -437,31 +427,29 @@ public:
     }
 
     void display_smt2(std::ostream & out, char const* module, param_descrs& descrs) const {
-        svector<params::entry>::const_iterator it  = m_entries.begin();  
+        for (params::entry const& e : m_entries) {
-        svector<params::entry>::const_iterator end = m_entries.end();
+            if (!descrs.contains(e.first)) continue;
-        for (; it != end; ++it) {
-            if (!descrs.contains(it->first)) continue;
             out << "(set-option :";
             out << module << ".";        
-            out << it->first;
+            out << e.first;
-            switch (it->second.m_kind) {
+            switch (e.second.m_kind) {
             case CPK_BOOL:
-                out << " " << (it->second.m_bool_value?"true":"false");
+                out << " " << (e.second.m_bool_value?"true":"false");
                 break;
             case CPK_UINT:
-                out << " " <<it->second.m_uint_value;
+                out << " " <<e.second.m_uint_value;
                 break;
             case CPK_DOUBLE:
-                out << " " << it->second.m_double_value;
+                out << " " << e.second.m_double_value;
                 break;
             case CPK_NUMERAL:
-                out << " " << *(it->second.m_rat_value);
+                out << " " << *(e.second.m_rat_value);
                 break;
             case CPK_SYMBOL:
-                out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);
+                out << " " << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value);
                 break;
             case CPK_STRING:
-                out << " " << it->second.m_str_value;
+                out << " " << e.second.m_str_value;
                 break;
             default:
                 UNREACHABLE();
@@ -472,29 +460,27 @@ public:
     }
 
     void display(std::ostream & out, symbol const & k) const {
-        svector<params::entry>::const_iterator it  = m_entries.begin();  
+        for (params::entry const& e : m_entries) {
-        svector<params::entry>::const_iterator end = m_entries.end();
+            if (e.first != k)
-        for (; it != end; ++it) {                                
-            if (it->first != k)
                 continue;
-            switch (it->second.m_kind) {
+            switch (e.second.m_kind) {
             case CPK_BOOL:
-                out << (it->second.m_bool_value?"true":"false");
+                out << (e.second.m_bool_value?"true":"false");
                 return;
             case CPK_UINT:
-                out << it->second.m_uint_value;
+                out << e.second.m_uint_value;
                 return;
             case CPK_DOUBLE:
-                out << it->second.m_double_value;
+                out << e.second.m_double_value;
                 return;
             case CPK_NUMERAL:
-                out << *(it->second.m_rat_value);
+                out << *(e.second.m_rat_value);
                 return;
             case CPK_SYMBOL:
-                out << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);
+                out << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value);
                 return;
             case CPK_STRING:
-                out << it->second.m_str_value;
+                out << e.second.m_str_value;
                 return;
             default:
                 out << "internal";
@@ -786,6 +772,7 @@ void params::del_values() {
     return false;                                               \
 }
 
+
 bool params::contains(symbol const & k) const {
     CONTAINS(k);
 }