Project

General

Profile

Bug #86

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

lustrev ne se termine pas

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

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

0%


Description

node Abs1_PP(
In1_1 : int;)
returns(
Out1_1 : int; );
var
Abs_1 : int;
let
Abs_1 = (if (In1_1 >= 0) then
In1_1
else (- In1_1));
Out1_1 = Abs_1;

tel

History

#1 Updated by Pierre-Loïc Garoche 3 months ago

  • Status changed from New to Closed

The example was not looping but generating an assert false
commit 72a93147f

Also available in: Atom PDF