From e1870233041a5a8cfb4fc7a0ab0c406e80d56eef Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 23 Jun 2018 21:57:10 -0700
Subject: [PATCH] fix #1699

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp    |  4 +++-
 src/opt/opt_pareto.cpp     |  2 ++
 src/tactic/sine_filter.cpp | 26 ++++++++------------------
 3 files changed, 13 insertions(+), 19 deletions(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index af28d2254..566aaa1f6 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -351,6 +351,7 @@ namespace opt {
     void context::get_model_core(model_ref& mdl) {
         mdl = m_model;
         fix_model(mdl);
+        mdl->set_model_completion(true);
         TRACE("opt", tout << *mdl;);
     }
 
@@ -528,7 +529,7 @@ namespace opt {
                     k += obj.m_weights[i];
                 }
                 else {
-                    TRACE("opt", tout << val << "\n";);
+                    TRACE("opt", tout << (*mdl)(obj.m_terms[i]) << "\n";);
                 }
             }
             if (is_ge) {
@@ -1539,6 +1540,7 @@ namespace opt {
         expr_ref tmp(m);
         model_ref mdl;
         get_model(mdl);
+        mdl->set_model_completion(true);
         for (expr * f : fmls) {
             if (!mdl->is_true(f)) {
                 //IF_VERBOSE(0, m_fm->display(verbose_stream() << "fm\n"));
diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp
index 56eed72ac..fe92c3ba6 100644
--- a/src/opt/opt_pareto.cpp
+++ b/src/opt/opt_pareto.cpp
@@ -40,6 +40,7 @@ namespace opt {
                     }
                     m_solver->get_model(m_model);
                     m_solver->get_labels(m_labels);
+                    m_model->set_model_completion(true);
                     IF_VERBOSE(1,
                                model_ref mdl(m_model);
                                cb.fix_model(mdl); 
@@ -99,6 +100,7 @@ namespace opt {
         if (is_sat == l_true) {
             m_solver->get_model(m_model);
             m_solver->get_labels(m_labels);
+            m_model->set_model_completion(true);
             mk_not_dominated_by();
         }
         return is_sat;
diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp
index 0ac726986..647791784 100644
--- a/src/tactic/sine_filter.cpp
+++ b/src/tactic/sine_filter.cpp
@@ -93,11 +93,8 @@ private:
                             obj_hashtable<func_decl> const & consts,
                             ptr_vector<func_decl> & next_consts) {
         TRACE("sine",
-            tout << "size of consts is "; tout << consts.size(); tout << "\n";
-            obj_hashtable<func_decl>::iterator it = consts.begin();
-            obj_hashtable<func_decl>::iterator end = consts.end();
-            for (; it != end; it++)
-                tout << *it << "\n"; );
+              tout << "size of consts is "; tout << consts.size(); tout << "\n";
+              for (func_decl* f : consts) tout << f->get_name() << "\n";);
 
         bool matched = false;
         for (unsigned i = 0; i < q->get_num_patterns(); i++) {
@@ -156,10 +153,8 @@ private:
                 if (!consts.contains(f)) {
                     consts.insert(f);
                     if (const2quantifier.contains(f)) {
-                        obj_pair_hashtable<expr, expr>::iterator it = const2quantifier[f].begin();
-                        obj_pair_hashtable<expr, expr>::iterator end = const2quantifier[f].end();
-                        for (; it != end; it++)
-                            stack.push_back(*it);
+                        for (auto const& p : const2quantifier[f]) 
+                            stack.push_back(p);
                         const2quantifier.remove(f);
                     }
                 }
@@ -220,16 +215,11 @@ private:
             visiting = to_visit.back();
             to_visit.pop_back();
             visited.insert(visiting);
-            obj_hashtable<func_decl>::iterator it = exp2const[visiting].begin();
-            obj_hashtable<func_decl>::iterator end = exp2const[visiting].end();
-            for (; it != end; it++) {
-                obj_hashtable<expr>::iterator exprit = const2exp[*it].begin();
-                obj_hashtable<expr>::iterator exprend = const2exp[*it].end();
-                for (; exprit != exprend; exprit++) {
-                    if (!visited.contains(*exprit))
-                        to_visit.push_back(*exprit);
+            for (func_decl* f : exp2const[visiting]) 
+                for (expr* e : const2exp[f]) {
+                    if (!visited.contains(e))
+                        to_visit.push_back(e);
                 }
-            }
         }
 
         for (unsigned i = 0; i < g->size(); i++) {