From c190d458596803fabc7db00d006c143e93b58e5d Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 4 Jan 2017 15:56:16 -0500
Subject: [PATCH] fix binary search string length axiom

---
 src/smt/theory_str.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 278f692f8..bfa439e03 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -9367,7 +9367,7 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT
             }
             if (lastBounds.midPoint.is_neg()) {
                 TRACE("t_str_binary_search", tout << "WARNING: length search converged on a negative value. Negating this constraint." << std::endl;);
-                expr_ref axiom(m.mk_not(ctx.mk_eq_atom(mk_strlen(freeVar), m_autil.mk_numeral(lastBounds.midPoint, true))), m);
+                expr_ref axiom(m_autil.mk_ge(mk_strlen(freeVar), m_autil.mk_numeral(rational::zero(), true)), m);
                 return axiom;
             }
             // length is fixed