From 347ea50b93cf3e66dbc004fba8fea804f1d53067 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 13 Aug 2017 09:25:46 -0700
Subject: [PATCH] fix for #1202

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_str.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 6f3dabe2e..aacf17b30 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8420,6 +8420,7 @@ namespace smt {
     // Check agreement between integer and string theories for the term a = (str.to-int S).
     // Returns true if axioms were added, and false otherwise.
     bool theory_str::finalcheck_str2int(app * a) {
+        SASSERT(u.str.is_stoi(a));
         bool axiomAdd = false;
         context & ctx = get_context();
         ast_manager & m = get_manager();
@@ -8446,7 +8447,10 @@ namespace smt {
             }
         } else {
             TRACE("str", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;);
-            NOT_IMPLEMENTED_YET();
+            expr_ref is_zero(ctx.mk_eq_atom(a, m_autil.mk_int(0)), m);
+            literal is_zero_l = mk_literal(is_zero);
+            axiomAdd = true;
+            // NOT_IMPLEMENTED_YET();
         }
 
         return axiomAdd;