Skip to content

Commit ff1fe63

Browse files
authored
Merge pull request #8348 from tautschnig/goto-synthesizer-going-to
goto-synthesizer: ignore __CPROVER_-prefixed symbols
2 parents 50bfa4e + 29cd187 commit ff1fe63

File tree

1 file changed

+18
-0
lines changed

1 file changed

+18
-0
lines changed

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Author: Qinheping Hu
1616
#include <util/find_symbols.h>
1717
#include <util/format_expr.h>
1818
#include <util/pointer_predicates.h>
19+
#include <util/prefix.h>
1920
#include <util/replace_symbol.h>
2021
#include <util/simplify_expr.h>
2122

@@ -158,6 +159,23 @@ void enumerative_loop_contracts_synthesizert::init_candidates()
158159
get_assigns(
159160
local_may_alias, loop_head_and_content.second, assigns_map[new_id]);
160161

162+
// Don't check assignable for CPROVER symbol
163+
for(auto it = assigns_map[new_id].begin();
164+
it != assigns_map[new_id].end();) // no ++it
165+
{
166+
if(auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(*it))
167+
{
168+
if(has_prefix(
169+
id2string(symbol_expr->get_identifier()), CPROVER_PREFIX))
170+
{
171+
it = assigns_map[new_id].erase(it);
172+
continue;
173+
}
174+
}
175+
176+
++it;
177+
};
178+
161179
// remove loop-local symbols from the inferred set
162180
cfg_info.erase_locals(assigns_map[new_id]);
163181

0 commit comments

Comments
 (0)