Skip to content

Commit afa3ad1

Browse files
author
martin
committed
Enable the use of assume for branches.
1 parent eb84546 commit afa3ad1

File tree

1 file changed

+3
-5
lines changed

1 file changed

+3
-5
lines changed

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -71,17 +71,15 @@ void variable_sensitivity_domaint::transform(
7171
case GOTO:
7272
{
7373
// TODO(tkiley): add support for flow sensitivity
74-
#if 0
75-
if (flow_sensitivity == FLOW_SENSITIVE)
74+
if (1) // (flow_sensitivity == FLOW_SENSITIVE)
7675
{
7776
locationt next=from;
7877
next++;
7978
if(next==to)
80-
assume(not_exprt(instruction.guard));
79+
abstract_state.assume(not_exprt(instruction.guard), ns);
8180
else
82-
assume(instruction.guard);
81+
abstract_state.assume(instruction.guard, ns);
8382
}
84-
#endif
8583
}
8684
break;
8785

0 commit comments

Comments
 (0)