File tree Expand file tree Collapse file tree 3 files changed +3
-3
lines changed
quantifiers-forall-ensures-01
quantifiers-forall-ensures-02 Expand file tree Collapse file tree 3 files changed +3
-3
lines changed Original file line number Diff line number Diff line change 1
- // clang-format oFF
1
+ // clang-format off
2
2
int f1 (int * arr ) __CPROVER_ensures (__CPROVER_forall {
3
3
int i ;
4
4
(0 <= i && i < 10 ) == > arr [i ] == 0
Original file line number Diff line number Diff line change 1
- // clang-format oFF
1
+ // clang-format off
2
2
int f1 (int * arr ) __CPROVER_ensures (__CPROVER_forall {
3
3
int i ;
4
4
(0 <= i && i < 10 ) == > arr [i ] == i
Original file line number Diff line number Diff line change @@ -171,7 +171,7 @@ void code_contractst::add_quantified_variable(
171
171
// If the expression is a quantified expression, this function adds
172
172
// the quantified variable to the symbol table and to the expression map
173
173
174
- // TODO Currently only works if the contract contains only a single
174
+ // TODO Currently only works if the contract contains only a single
175
175
// quantified formula
176
176
// i.e. (1) the top-level element is a quantifier formula
177
177
// and (2) there are no inner quantifier formulae
You can’t perform that action at this time.
0 commit comments