set uninitialized fields. Maybe related to #1468

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

src/interp/iz3interp.cpp

@@ -255,9 +255,11 @@ public:
             throw interpolation_failure(msg);
         }
         catch (const iz3translation::unsupported &) {
+            TRACE("iz3", tout << "unsupported\n";);
             throw interpolation_error();
         }
         catch (const iz3proof::proof_error &) {
+            TRACE("iz3", tout << "proof error\n";);
             throw interpolation_error();
         }
         profiling::timer_stop("Proof translation");
@@ -304,9 +306,11 @@ public:
                 throw interpolation_failure(msg);
             }
             catch (const iz3translation::unsupported &) {
+                TRACE("iz3", tout << "unsupported\n";);
                 throw interpolation_error();
             }
             catch (const iz3proof::proof_error &) {
+                TRACE("iz3", tout << "proof error\n";);
                 throw interpolation_error();
             }
             profiling::timer_stop("Proof translation");

src/interp/iz3translate.cpp

@@ -983,6 +983,7 @@ public:
     ast get_bounded_variable(const ast &ineq, bool &lb){
         ast nineq = normalize_inequality(ineq);
         ast lhs = arg(nineq,0);
+        lhs.raw();
         switch(op(lhs)){
         case Uninterpreted: 
             lb = false;
@@ -993,10 +994,10 @@ public:
             else if(arg(lhs,0) == make_int(rational(-1)))
                 lb = true;
             else 
-                throw unsupported();
+                throw unsupported(lhs);
             return arg(lhs,1);
         default:
-            throw unsupported();
+            throw unsupported(lhs);
         }
     }
 
@@ -1101,10 +1102,10 @@ public:
         rational xcoeff = get_first_coefficient(arg(x,0),xvar);
         rational ycoeff = get_first_coefficient(arg(y,0),yvar);
         if(xcoeff == rational(0) || ycoeff == rational(0) || xvar != yvar)
-            throw unsupported();  // can be caused by non-linear arithmetic
+            throw unsupported(x);  // can be caused by non-linear arithmetic
         rational ratio = xcoeff/ycoeff;
         if(denominator(ratio) != rational(1))
-            throw unsupported(); // can this ever happen?
+            throw unsupported(y); // can this ever happen?
         return make_int(ratio); // better be integer!
     }
 
@@ -1113,7 +1114,7 @@ public:
         get_assign_bounds_coeffs(proof,farkas_coeffs);
         int nargs = num_args(con);
         if(nargs != (int)(farkas_coeffs.size()))
-            throw unsupported(); // should never happen
+            throw unsupported(proof); // should never happen
 #if 0
         if(farkas_coeffs[0] != make_int(rational(1)))
             farkas_coeffs[0] = make_int(rational(1));
@@ -1237,7 +1238,7 @@ public:
         if(pr(rew) == PR_REWRITE){
             return clause; // just hope the rewrite does nothing!
         }
-        throw unsupported();
+        throw unsupported(rew);
     }
 
 
@@ -1311,7 +1312,7 @@ public:
   
     ast commute_equality_iff(const ast &con){
         if(op(con) != Iff || op(arg(con,0)) != Equal)
-            throw unsupported();
+            throw unsupported(con);
         return make(Iff,commute_equality(arg(con,0)),commute_equality(arg(con,1)));
     }
   
@@ -1337,7 +1338,7 @@ public:
             prs.push_back(con);
             return clone(proof,prs);
         default:
-            throw unsupported();
+            throw unsupported(proof);
         }
     }
 
@@ -1837,7 +1838,7 @@ public:
             for(unsigned i = 0; i < nprems; i++)
                 if(sym(args[i]) == commute
                    && !(dk == PR_TRANSITIVITY || dk == PR_MODUS_PONENS || dk == PR_SYMMETRY ||  (dk == PR_MONOTONICITY && op(arg(con,0)) == Not)))
-                    throw unsupported();
+                    throw unsupported(proof);
 
             switch(dk){
             case PR_TRANSITIVITY: {
@@ -1908,7 +1909,7 @@ public:
                             int nargs = num_args(con);
                             if(farkas_coeffs.size() != (unsigned)nargs){
                                 pfgoto(proof);
-                                throw unsupported();
+                                throw unsupported(proof);
                             }
                             for(int i = 0; i < nargs; i++){
                                 ast lit = mk_not(arg(con,i));
@@ -1946,7 +1947,7 @@ public:
                         get_broken_gcd_test_coeffs(proof,farkas_coeffs);
                         if(farkas_coeffs.size() != nprems){
                             pfgoto(proof);
-                            throw unsupported();
+                            throw unsupported(proof);
                         }
                         std::vector<Iproof::node> my_prems; my_prems.resize(2);
                         std::vector<ast> my_prem_cons; my_prem_cons.resize(2);
@@ -1969,7 +1970,7 @@ public:
                         if(args.size() > 0)
                             res =  GomoryCutRule2Farkas(proof, conc(proof), args);
                         else
-                            throw unsupported();
+                            throw unsupported(proof);
                         break;
                     }
                     case EqPropagateKind: {
@@ -1988,7 +1989,7 @@ public:
                         break;
                     }
                     default:
-                        throw unsupported();
+                        throw unsupported(proof);
                     }
                     break;
                 case ArrayTheory: {// nothing fancy for this
@@ -2000,7 +2001,7 @@ public:
                     break;
                 }
                 default:
-                    throw unsupported();
+                    throw unsupported(proof);
                 }
                 break;
             }
@@ -2024,7 +2025,7 @@ public:
                 if(is_local(con))
                     res = args[0];
                 else
-                    throw unsupported();
+                    throw unsupported(con);
                 break;
             }
             case PR_COMMUTATIVITY: {
@@ -2048,7 +2049,7 @@ public:
                 IF_VERBOSE(0, verbose_stream() << "Unsupported proof rule: " << expr_ref((expr*)proof.raw(), *proof.mgr()) << "\n";);
                 //                pfgoto(proof);                
                 // SASSERT(0 && "translate_main: unsupported proof rule");
-                throw unsupported();
+                throw unsupported(proof);
             }
         }
 

src/interp/iz3translate.h

@@ -36,7 +36,8 @@ class iz3translation : public iz3base {
 
     /** This is thrown when the proof cannot be translated. */
     struct unsupported: public iz3_exception {
-    unsupported(): iz3_exception("unsupported") { }
+        raw_ast* m_ast;
+    unsupported(ast const& a): iz3_exception("unsupported"), m_ast(a.raw()) { }
     };
 
     static iz3translation *create(iz3mgr &mgr,

src/sat/sat_clause.cpp

@@ -33,6 +33,8 @@ namespace sat {
         m_frozen(false),
         m_reinit_stack(false),
         m_inact_rounds(0) {
+        m_psm = 0;
+        m_glue = 0;
         memcpy(m_lits, lits, sizeof(literal) * sz);
         mark_strengthened();
         SASSERT(check_approx());

src/sat/sat_solver.cpp

@@ -2460,10 +2460,7 @@ namespace sat {
             // try to use cached implication if available
             literal_vector * implied_lits = m_probing.cached_implied_lits(~l);
             if (implied_lits) {
-                literal_vector::iterator it  = implied_lits->begin();
+                for (literal l2 : *implied_lits) {
-                literal_vector::iterator end = implied_lits->end();
-                for (; it != end; ++it) {
-                    literal l2 = *it;
                     // Here, we must check l0 != ~l2.
                     // l \/ l2 is an implied binary clause.
                     // However, it may have been deduced using a lemma that has been deleted.