Skip to content

Commit

Permalink
Adapt to e53bbfe
Browse files Browse the repository at this point in the history
  • Loading branch information
schuessf committed Nov 8, 2024
1 parent 25e8923 commit d19095a
Showing 1 changed file with 4 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -422,8 +422,9 @@ private static void createNewEdge(final Multigraph<String, BoogieASTNode> source
}

private static Multigraph<String, BoogieASTNode> createWitnessNode(final IcfgLocation old) {
final WitnessInvariant inv = WitnessInvariant.getAnnotation(old);
final Multigraph<String, BoogieASTNode> rtr = new Multigraph<>(inv == null ? null : inv.getInvariant());
final WitnessInvariant<?> inv = WitnessInvariant.getAnnotation(old);
final Multigraph<String, BoogieASTNode> rtr =
new Multigraph<>(inv == null ? null : inv.getInvariant().toString());
ModelUtils.copyAnnotations(old, rtr);
return rtr;
}
Expand All @@ -432,6 +433,7 @@ private static Multigraph<String, BoogieASTNode> createWitnessNode(final IcfgLoc
public Expression translateExpression(final Term term) {
return mTerm2Expression.translate(term);
}

// TODO maybe take getStepInfoFromCondition from BoogiePreprocessorBacktranslator
private StepInfo getStepInfoFromCondition(final Expression input, final Expression output) {
// compare the depth of UnaryExpression in the condition of the assume
Expand Down

0 comments on commit d19095a

Please sign in to comment.