From 5f78ca9b588d3d0a7405e39630d548477f750710 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 25 Nov 2019 14:28:44 -0500
Subject: [PATCH] z3str3: negative lengths in get_len_value don't count
---
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 ff67ded9c..d68641166 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -5061,7 +5061,7 @@ namespace smt {
}
TRACE("str", tout << "length of " << mk_ismt2_pp(e, m) << " is " << val << std::endl;);
- return val.is_int();
+ return val.is_int() && val.is_nonneg();
}
/*