fix crash in poly normalizer exposed by qe. Issue #775

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

src/ast/simplifier/arith_simplifier_plugin.cpp

@@ -43,8 +43,7 @@ bool arith_simplifier_plugin::is_neg_poly(expr * t) const {
     if (m_util.is_mul(t)) {
         t = to_app(t)->get_arg(0);
         rational r;
-        bool is_int;
+        if (is_numeral(t, r))
-        if (m_util.is_numeral(t, r, is_int))
             return r.is_neg();
     }
     return false;

src/ast/simplifier/poly_simplifier_plugin.cpp

@@ -607,12 +607,25 @@ void poly_simplifier_plugin::append_to_monomial(expr * n, numeral & k, ptr_buffe
     k *= val;
     n  = get_monomial_body(n);
 
-    if (is_mul(n)) {
+    unsigned hd = result.size();
-        for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
+    result.push_back(n);
-            result.push_back(to_app(n)->get_arg(i));
+    while (hd < result.size()) {
-    }
+        n = result[hd];
-    else {
+        if (is_mul(n)) {
-        result.push_back(n);
+            result[hd] = result.back();
+            result.pop_back();
+            for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) {
+                result.push_back(to_app(n)->get_arg(i));
+            }
+        }
+        else if (is_numeral(n, val)) {
+            k *= val;
+            result[hd] = result.back();
+            result.pop_back();
+        }
+        else {
+            ++hd;
+        }
     }
 }
 

src/smt/theory_seq.cpp

@@ -1815,7 +1815,10 @@ bool theory_seq::solve_ne(unsigned idx) {
     for (unsigned i = 0; i < n.lits().size(); ++i) {
         switch (ctx.get_assignment(n.lits(i))) {
         case l_false:
-            TRACE("seq", display_disequation(tout << "has false literal\n", n););
+            TRACE("seq", display_disequation(tout << "has false literal\n", n);
+                  ctx.display_literal_verbose(tout, n.lits(i));                  
+                  tout << "\n" << n.lits(i) << " " << ctx.is_relevant(n.lits(i)) << "\n";
+                  );
             return true;
         case l_true:
             break;
@@ -1841,7 +1844,10 @@ bool theory_seq::solve_ne(unsigned idx) {
         change = canonize(n.rs(i), rs, deps) || change;
 
         if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, change)) {
-            TRACE("seq", display_disequation(tout << "reduces to false: ", n););
+            TRACE("seq", display_disequation(tout << "reduces to false: ", n);
+                  tout << n.ls(i) << " -> " << ls << "\n";
+                  tout << n.rs(i) << " -> " << rs << "\n";);
+
             return true;
         }
         else if (!change) {
@@ -3720,30 +3726,29 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
     expr_ref e2(n2->get_owner(), m);
     m_exclude.update(e1, e2);
     expr_ref eq(m.mk_eq(e1, e2), m);
+    TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";);
     m_rewrite(eq);
     if (!m.is_false(eq)) {
-        TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";);
 
         literal lit = mk_eq(e1, e2, false);
 
-        // propagate x != "" into x = (++ (unit (nth x 0) (tail x 0)))
         if (m_util.str.is_empty(e2)) {
             std::swap(e1, e2);
         }
+#if 0
         if (false && m_util.str.is_empty(e1)) {
             expr_ref head(m), tail(m), conc(m);
             mk_decompose(e2, head, tail);
             conc = mk_concat(head, tail);
             propagate_eq(~lit, e2, conc, true);
         }
-#if 0
+
         // (e1 = "" & e2 = xdz) or (e2 = "" & e1 = xcy) or (e1 = xcy & e2 = xdz & c != d) or (e1 = x & e2 = xdz) or (e2 = x & e1 = xcy)
         // e1 = "" or e1 = xcy or e1 = x
         // e2 = "" or e2 = xdz or e2 = x
         // e1 = xcy or e2 = xdz
         // c != d
 
-        literal lit = mk_seq_eq(e1, e2);
         sort* char_sort = 0;
         expr_ref emp(m);
         VERIFY(m_util.is_seq(m.get_sort(e1), char_sort));