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(); } /*