Project

General

Profile

« Previous | Next » 

Revision 97602f7c

Added by Guillaume Davy over 9 years ago

Correct bug when there is no precondition and change reprensentation
of boolean in ACSL

View differences:

tcm_benchmarks/ALT2/ALT2_proof/ALT_2.lustrec.coq
208 208
eassumption.
209 209
Qed.
210 210

  
211
Goal typed_ref_AltitudeControl_step_stmt_post_5.
211
Goal typed_ref_AltitudeControl_step_stmt_post.
212 212
Hint AltitudeControl_step,default,property.
213 213
Proof.
214
  Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;why3 "CVC4" timelimit 10.
214
(* Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;why3 "CVC4" timelimit 10. *)
215 215
Qed.
216 216

  
217
Goal typed_ref_VariableRateLimit_step_stmt_post.
217
Goal typed_ref_VariableRateLimit_step_stmt_post_4.
218 218
Hint VariableRateLimit_step,default,property.
219 219
Proof.
220 220
(* Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;why3 "CVC4" timelimit 10. *)
221 221
Qed.
222 222

  
223
Goal typed_ref_integrator_reset_step_stmt_post_2.
224
Hint default,integrator_reset_step,property.
225
Proof.
226
  Require Why3. intros. hnf. repeat split;try why3 "CVC3" timelimit 10;try why3 "Z3" timelimit 10;why3 "CVC4" timelimit 10.
227
Qed.
228

  
229 223

  

Also available in: Unified diff