Project

General

Profile

« Previous | Next » 

Revision 3e209698

Added by Pierre-Loïc Garoche almost 9 years ago

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.

View differences:

test/tests_ok.list
894 894
./src/kind_fmcad08/protocol/swimmingpool_2.lus,top
895 895
./src/kind_fmcad08/protocol/rtp_1.lus,top
896 896
./src/kind_fmcad08/protocol/swimmingpool_7.lus,top
897
./src/arrays_arnaud/arrays.lus,,-check-access
898
./src/arrays_arnaud/RelOpMatrix.lus
899
./src/arrays_arnaud/access1.lus,,-check-access
900
./src/arrays_arnaud/generic1.lus
901
./src/arrays_arnaud/generic2.lus
902
./src/arrays_arnaud/generic3.lus,top,-dynamic -check-access
903
./src/clocks/clocks1.lus
904
./src/clocks/clocks2.lus
905
./src/clocks/oversampling0.lus

Also available in: Unified diff