Project

General

Profile

Bug #85

Bug #84: kind2 output : "real when true(_isEnabled_clock)" => "real"

lustrev failed

Added by Hamza Bourbouh 5 months ago. Updated 5 months ago.

Status:
Closed
Priority:
Normal
Category:
Bug
Start date:
07/16/2019
Due date:
% Done:

0%


Description

lustrev -verbose 0 -seal -seal-export lustre -d toto2 -node Clock_PP Clock_PP.LUSTREC.lus
Raised by primitive operation at file "arg.ml", line 281, characters 4-31
Called from file "main_lustre_verifier.ml", line 133, characters 4-37
Fatal error: exception File "tools/seal/seal_extract.ml", line 582, characters 7-13: Assertion failed
Raised by primitive operation at file "arg.ml", line 281, characters 4-31
Called from file "main_lustre_verifier.ml", line 133, characters 4-37

History

#1 Updated by Hamza Bourbouh 5 months ago

  • Status changed from New to Closed
Comment

fixed in lustrec-seal branch

Also available in: Atom PDF