Revision 3e209698
Added by Pierre-Loïc Garoche almost 9 years ago
| 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
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.