From 6948699ec6dc95736e848ccf9dc533bcbdfa1424 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Sat, 5 Apr 2025 06:32:49 +0000 Subject: [PATCH] Replace conditions in quantified statement expressions --- .../cbmc/Quantifiers-statement-expression/main.c | 2 +- src/ansi-c/goto-conversion/goto_clean_expr.cpp | 13 +++++-------- 2 files changed, 6 insertions(+), 9 deletions(-) diff --git a/regression/cbmc/Quantifiers-statement-expression/main.c b/regression/cbmc/Quantifiers-statement-expression/main.c index 3222418c54f..efd5c55f9ca 100644 --- a/regression/cbmc/Quantifiers-statement-expression/main.c +++ b/regression/cbmc/Quantifiers-statement-expression/main.c @@ -4,7 +4,7 @@ int main() // no side effects! int j = 0; int a[5] = {0 , 0, 0, 0, 0}; - assert(__CPROVER_forall { int i; ({ int j = i; i=i; if(i < 0 || i >4) i = 1; ( a[i] < 5); }) }); + assert(__CPROVER_forall { int i; ({ int j = i; int cond = i < 0 || i >4; if(cond) i = 1; ( a[i] < 5); }) }); // clang-format on return 0; diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index ff976217d34..4a605141902 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -211,19 +211,16 @@ static exprt convert_statement_expression( // path_condition && cond. case goto_program_instruction_typet::GOTO: { - if(!current_it->condition().is_true()) + exprt condition = current_it->condition(); + replace_expr(value_map, condition); + if(!condition.is_true()) { auto next_it = current_it->targets.front(); exprt copy_path_condition = path_condition; - replace_mapt copy_symbol_map = value_map; - auto copy_condition = current_it->condition(); - path_condition = - and_exprt(path_condition, not_exprt(current_it->condition())); + path_condition = and_exprt(path_condition, not_exprt(condition)); current_it++; paths.push_back( - next_it, - and_exprt(copy_path_condition, copy_condition), - copy_symbol_map); + next_it, and_exprt(copy_path_condition, condition), value_map); } else {