| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / @ 953879f0

History | View | Annotate | Download (7.65 KB)

# Date Author Comment
07ceae4c 07/13/2017 05:47 PM Pierre-Loïc Garoche

[HORN] Protect names of stateless nodes with a _fun suffix. This was conflicting with existing names in Z3, ie. "abs".
[HORN] Better treatment of stateless nodes collecting semantics
Fixes issue #13 on github:

d2d9d4cb 04/26/2017 11:25 PM Pierre-Loïc Garoche

Missing files

ca88e660 01/08/2016 05:37 PM Pierre-Loïc Garoche

Resolved conflict when merging salsa with horn_encoding. The current branch is the most updated.

0dee2bc1 11/20/2015 06:41 PM Pierre-Loïc Garoche

Refactoring of the horn backend with Reset/Step instead of Init/Step.
Teme, please perform a string non regression test wrt the previous version, to make sure we have the same model checking results.