Skip to content

Commit 94f99b5

Browse files
Adding forgotten precondition in not_contains constraint
1 parent d4a9b2a commit 94f99b5

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/solvers/refinement/string_constraint_generator_indexof.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -260,8 +260,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
260260
{
261261
string_not_contains_constraintt a4(
262262
plus_exprt(offset, from_integer(1, index_type)),
263-
from_index,
264263
plus_exprt(end_index, from_integer(1, index_type)),
264+
contains,
265265
from_integer(0, index_type),
266266
needle.length(),
267267
haystack,

0 commit comments

Comments
 (0)