trace down recent exposed regression in goal2sat, incorporate Scott's suggestion on making vector<std::string inaccessible

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

src/model/func_interp.cpp

@@ -107,13 +107,10 @@ void func_interp::reset_interp_cache() {
 
 bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
     args.reset();
-    if (!is_app(e) || !m().is_ite(to_app(e)))
+    expr* c, *t, *f;
+    if (!m().is_ite(e, c, t, f)) {
         return false;
-
+    }
-    app * a = to_app(e);
-    expr * c = a->get_arg(0);
-    expr * t = a->get_arg(1);
-    expr * f = a->get_arg(2);
 
     if ((m_arity == 0) ||
         (m_arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) ||

src/qe/qe_arith.cpp

@@ -32,7 +32,6 @@ namespace qe {
 
     bool is_divides(arith_util& a, expr* e1, expr* e2, rational& k, expr_ref& p) {  
         expr* t1, *t2;
-        ast_manager& m = a.get_manager();
         if (a.is_mod(e2, t1, t2) && 
             a.is_numeral(e1, k) && 
             k.is_zero() &&

src/qe/qe_datatypes.cpp

@@ -87,7 +87,6 @@ namespace qe {
         }
 
         void project_rec(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
-            func_decl* f = m_val->get_decl();
             expr_ref rhs(m);
             expr_ref_vector eqs(m);
             for (unsigned i = 0; i < lits.size(); ++i) {

src/sat/tactic/goal2sat.cpp

@@ -324,6 +324,7 @@ struct goal2sat::imp {
     }
     
     void process(expr * n) {
+        //SASSERT(m_result_stack.empty());
         TRACE("goal2sat", tout << "converting: " << mk_ismt2_pp(n, m) << "\n";);
         if (visit(n, true, false)) {
             SASSERT(m_result_stack.empty());
@@ -342,8 +343,7 @@ struct goal2sat::imp {
             bool sign  = fr.m_sign;
             TRACE("goal2sat_bug", tout << "result stack\n";
                   tout << mk_ismt2_pp(t, m) << " root: " << root << " sign: " << sign << "\n";
-                  for (unsigned i = 0; i < m_result_stack.size(); i++) tout << m_result_stack[i] << " ";
+                  tout << m_result_stack << "\n";);
-                  tout << "\n";);
             if (fr.m_idx == 0 && process_cached(t, root, sign)) {
                 m_frame_stack.pop_back();
                 continue;
@@ -362,11 +362,11 @@ struct goal2sat::imp {
             }
             TRACE("goal2sat_bug", tout << "converting\n";
                   tout << mk_ismt2_pp(t, m) << " root: " << root << " sign: " << sign << "\n";
-                  for (unsigned i = 0; i < m_result_stack.size(); i++) tout << m_result_stack[i] << " ";
+                  tout << m_result_stack << "\n";);
-                  tout << "\n";);
             convert(t, root, sign);
             m_frame_stack.pop_back();
         }
+        CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";);
         SASSERT(m_result_stack.empty());
     }
 

src/smt/theory_seq.cpp

@@ -298,7 +298,6 @@ final_check_status theory_seq::final_check_eh() {
 
 bool theory_seq::reduce_length_eq() {
     context& ctx = get_context();
-    unsigned sz = m_eqs.size();
     int start = ctx.get_random_value();
 
     for (unsigned i = 0; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
@@ -457,7 +456,6 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
 }
 
 bool theory_seq::branch_variable_mb() {
-    context& ctx = get_context();
     bool change = false;
     for (unsigned i = 0; i < m_eqs.size(); ++i) {
         eq const& e = m_eqs[i];
@@ -2208,7 +2206,6 @@ bool theory_seq::check_int_string() {
 }
 
 bool theory_seq::add_itos_axiom(expr* e) {
-    context& ctx = get_context();
     rational val;
     expr* n;
     VERIFY(m_util.str.is_itos(e, n));

src/util/vector.h

@@ -457,5 +457,15 @@ template<typename Hash>
 struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
 
 
+// Specialize vector<std::string> to be inaccessible.
+// This will catch any regression of issue #564 and #420.
+// Use std::vector<std::string> instead.
+template <>
+class vector<std::string, true, unsigned> {
+private:
+    vector<std::string, true, unsigned>();
+};
+
+
 #endif /* VECTOR_H_ */