Commit 98f0035
committed
Fix statement-expression expansion for Kani-provided quantifiers
CBMC side of model-checking/kani#4020:
re-using the same converter instance would confuse finish-gotos (when
really we don't want gotos inside the statement expression to be
considered at all by the main goto-converter instances).1 parent f1faa61 commit 98f0035
1 file changed
+5
-2
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
61 | 61 | | |
62 | 62 | | |
63 | 63 | | |
64 | | - | |
| 64 | + | |
| 65 | + | |
65 | 66 | | |
66 | 67 | | |
| 68 | + | |
67 | 69 | | |
68 | 70 | | |
69 | 71 | | |
| |||
716 | 718 | | |
717 | 719 | | |
718 | 720 | | |
719 | | - | |
| 721 | + | |
| 722 | + | |
720 | 723 | | |
721 | 724 | | |
722 | 725 | | |
| |||
0 commit comments