From 72f8e408fc39afca1f5c690b20fd86e3518ac687 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 17 Mar 2018 11:25:07 -0700
Subject: [PATCH] fix #1538

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context_pp.cpp | 6 +++---
 src/smt/theory_seq.cpp     | 8 ++++----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index f072a1d13..f4f56df5d 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -580,20 +580,20 @@ namespace smt {
         case b_justification::BIN_CLAUSE: {
             literal l2 = j.get_literal();
             out << "bin-clause ";
-            display_literal(out, l2);
+            display_literal_verbose(out, l2);
             break;
         }
         case b_justification::CLAUSE: {
             clause * cls = j.get_clause();
             out << "clause ";
-            if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals());
+            if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
             break;
         }
         case b_justification::JUSTIFICATION: {
             out << "justification " << j.get_justification()->get_from_theory() << ": ";
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
-            display_literals(out, lits);
+            display_literals_verbose(out, lits);
             break;
         }
         default:
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index b90735a07..94841603d 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2404,8 +2404,7 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
             lits.push_back(~is_digit(ith_char));
             nums.push_back(digit2int(ith_char));
         }        
-        for (unsigned i = sz-1, c = 1; i > 0; c *= 10) {
-            --i;
+        for (unsigned i = sz, c = 1; i-- > 0; c *= 10) {
             coeff = m_autil.mk_int(c);
             nums[i] = m_autil.mk_mul(coeff, nums[i].get());
         }
@@ -2414,9 +2413,10 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
         lits.push_back(mk_eq(e, num, false));
         ++m_stats.m_add_axiom;
         m_new_propagation = true;
-        for (unsigned i = 0; i < lits.size(); ++i) {
-            ctx.mark_as_relevant(lits[i]);
+        for (literal lit : lits) {
+            ctx.mark_as_relevant(lit);
         }
+        TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
         ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
         m_stoi_axioms.insert(val);
         m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val));