Skip to content

Commit 16f971b

Browse files
Only add axioms for testing functions
1 parent 6587b31 commit 16f971b

File tree

1 file changed

+5
-2
lines changed

1 file changed

+5
-2
lines changed

src/solvers/refinement/string_refinement_util.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -399,7 +399,10 @@ void string_dependenciest::add_constraints(
399399
{
400400
for(const auto &builtin : builtin_function_nodes)
401401
{
402-
const exprt return_value = builtin.data->add_constraints(generator);
403-
generator.add_lemma(equal_exprt(return_value, builtin.data->return_code));
402+
if(builtin.data->maybe_testing_function())
403+
{
404+
const exprt return_value = builtin.data->add_constraints(generator);
405+
generator.add_lemma(equal_exprt(return_value, builtin.data->return_code));
406+
}
404407
}
405408
}

0 commit comments

Comments
 (0)