From 14f542efee842d72e114bc25ee74ce76f4047c38 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Feb 2019 10:57:08 +0000 Subject: [PATCH] String refinement: Do not fail if the solver returns a negative string length The string length may initially be unconstrained, and such counterexamples should not result in failing invariants. When enabling field sensitivity, strings-smoke-tests/java_index_of2 was failing as the solver returned -1073741820 for string_refinement#string_length#1 (which is a signed integer). --- src/solvers/strings/string_refinement.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 8c6e227793d..11035f7b03c 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -1213,6 +1213,12 @@ static exprt negation_of_not_contains_constraint( // The negated existential becomes an universal, and this is the unrolling of // that universal quantifier. + // Ff the upper bound is smaller than the lower bound (specifically, it might + // actually be negative as it is initially unconstrained) then there is + // nothing to do (and the reserve call would fail). + if(ube < lbe) + return and_exprt(univ_bounds, get(constraint.premise)); + std::vector conjuncts; conjuncts.reserve(numeric_cast_v(ube - lbe)); for(mp_integer i = lbe; i < ube; ++i)