Project

General

Profile

Edit Actions

Bug #85

closed

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

lustrev failed

Added by Hamza Bourbouh almost 3 years ago. Updated 2 days ago.

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

0%

Estimated time:

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

Edit Actions

Also available in: Atom PDF