Updated version of test script: timeout for z3
Fixed bug on the main part
Cleaning useless files
First fully working version of horn backend.
Has to be called with "-horn -node main_node"
The test script compute the smt2 file and calls z3 on them.
Is it working?
Working on bugs
Manually corrected version of ex3. Should integrate the modifications
Second (almost) working version
First (almost) working version
In the middle of the coding process. Just pushing thinks
The missing file
Initial copy of the horn output version. Not really working yet
lego robot example
missing dummy lib for arrays
- Renamed the only target of the generated makefile- Solved bug: xor are now printed as bitwise xor in c : a ^ b and not a xor b.
- work in progress for interface typing
- small bug correction in dimension typing - #open keyword instead of open - dummy generic matrix/vector library interface added - modified examples according to the new syntax
Merge (if it works) of the lustre interfaces branche providing lusi files into trunk
Lustre interfaces: lusi files are generated and used. Remaining work: create a good makefile and add the appropriate #include, fix issues with Arnaud's benchmarks (old syntax)
Moved files to trunk in lustre_compiler