CristalCaveGem » LustreC

moved from Num to Zarith. IMpacted main.ml ad uses of Z3 in zustre_cex and seal-extract

printing nodes + more progress on seal export

- Refactored Error exception and messages
- Bugs in partial evaluation for equalities among bool constants
and a nice recursive call generating a stack overflow! Now solved
- Setup a timeout for z3 in seal
- Better log for seal

Commenting out unused variables

[seal] more progress on seal extract

seal: now deals with enum

[seal] delt with Merge and when
[printer] more kind2 syntax

Output folder for seal-extract

Zustre: Bug solved in const injection for reals

lustrev seal: ongoing work on extraction as dynamical system. Still not working yet

Fixing issues with changes in machine code

Added two fresh vars counter and uid.
uid is a list of integer denoting the specific instance of a stateful/stateless node.

New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation

missing file

Zustre: timeout and slicing

zustre progress. Issues with sliced predicates

package z3 to Z3 when using z3 github repo.

Adding input in MAIN fdecl

[lustrev] fixed some issues when calling Z3. Seems working for the moment: basic call to Z3 and sat/unsat result

Some progress on zustre

Try to debug the use of Z3 API. Still having troubles

Zustre: do not declare variables as Fixedpoint relations

Filtering out ERR and MAIN from the forall quantification

Some progress on zustre2