File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -218,13 +218,13 @@ let t_bdhoare_while_rev_geq_r inv vrnt (k: ss_inv) (eps: ss_inv) tc =
218218
219219 if not (PV. indep env (s_write env lp_body) (PV. fv env (EcMemory. memory mem) eps.inv)) then
220220 tc_error !! tc
221- " The variant decreasing rate lower-bound cannot "
222- " depend on variables written by the loop body" ;
221+ " The variant decreasing rate lower-bound cannot \
222+ depend on variables written by the loop body" ;
223223
224224 if not (PV. indep env (s_write env lp_body) (PV. fv env (EcMemory. memory mem) k.inv)) then
225225 tc_error !! tc
226- " The variant upper bound cannot depend on "
227- " variables written by the loop body" ;
226+ " The variant upper bound cannot depend on \
227+ variables written by the loop body" ;
228228
229229 check_single_stmt tc rem_s;
230230
You can’t perform that action at this time.
0 commit comments