All issues

Search results

How can I use zustre to verify whether a lustre program satisfy the FRETish specifications?

Status: Open.

#14 In coco-team/zustre;

· Atmanuclear opened on Apr 24, 2023

About newer version of zustre

Status: Open.

#13 In coco-team/zustre;

· kumori123 opened on Aug 24, 2022

Z3Exception: invalid rational value passed as an integer

Status: Open.

#12 In coco-team/zustre;

· daniel-larraz opened on Jul 16, 2017

assert is_uninterpreted (decl) in fp_get_preds function (utils.py)

Status: Open.

#11 In coco-team/zustre;

· ploc opened on Jul 13, 2017

Output type of top node is ignored

Status: Open.

#10 In coco-team/zustre;

· daniel-larraz opened on Jun 23, 2017

Zustre raises an exception if input program does not include a node called 'top'

Status: Open.

#9 In coco-team/zustre;

· daniel-larraz opened on Jun 22, 2017

Zustre generates a malformed SMT2 problem if input program does not contain arrow operators

Status: Open.

#8 In coco-team/zustre;

· daniel-larraz opened on Jun 22, 2017

return code of Zustre

Status: Open.

#6 In coco-team/zustre;

· hbourbouh opened on Feb 7, 2017

CoCoSpec generation in stateless programs

Status: Open.

#1 In coco-team/zustre;

· lememta opened on Jul 17, 2016