tests require super_prove, which requires python-pip, which isn't available on ubuntu 20.04

[programmerjake]

The installation instructions should be updated, or maybe super_prove should be changed to an optional dependency for running tests.

[jix]

Thank you for reporting this, I appreciate hearing about any issues in getting the sby tests setup.

The individual solvers are already optional dependencies for the test suite. If a solver executable is not found in the path, running a test for it should produce an output like SKIPPING regression/aim_vs_smt2_nonzero_start_offset_aiger_suprove: `suprove` not found and continue without failing the tests.

Currently the test setup never rescans for solvers after running the tests once. If you had a non-working suprove in your PATH when running the tests for the first time, you can delete the tests/make/rules directory manually to force it to regenerate the make rules according to the solvers currently present. That should not be required and I'll fix this.

Let me know if you don't have suprove in your path and this issue persist even after deleting tests/make/rules. In that case there must be another issue.

Regarding the installation instructions, I agree that there is room for improvement. While it currently does say that only yosys and z3 are required dependencies at the beginning, it scrolls right past that if you navigate via the "Prerequisites" link from the table of contents. It also doesn't mention the OSS CAD Suite which is recommended as it bundles the same solver versions used for the CI setup. I will look into updating this.

[programmerjake]

Well, the optional dependency checking is apparently broken (on ad2c33d):

~$ suprove
suprove: command not found
~$ cd /tmp
/tmp$ git clone https://github.com/YosysHQ/sby
...
/tmp$ cd sby
/tmp/sby$ make ci
...
cd sbysrc && python3 sby.py -f demo2.sby
SBY  2:37:45 [demo2] Removing directory '/tmp/sby/sbysrc/demo2'.
SBY  2:37:45 [demo2] Writing 'demo2/src/demo.v'.
SBY  2:37:45 [demo2] engine_0: aiger suprove
SBY  2:37:45 [demo2] engine_1: aiger avy
SBY  2:37:45 [demo2] base: starting process "cd demo2/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  2:37:45 [demo2] base: finished (returncode=0)
SBY  2:37:45 [demo2] aig: starting process "cd demo2/model; yosys -ql design_aiger.log design_aiger.ys"
SBY  2:37:45 [demo2] aig: finished (returncode=0)
SBY  2:37:45 [demo2] engine_0: starting process "cd demo2; suprove model/design_aiger.aig"
SBY  2:37:45 [demo2] engine_1: starting process "cd demo2; avy --cex - model/design_aiger.aig"
SBY  2:37:45 [demo2] engine_0: finished (returncode=127)
SBY  2:37:45 [demo2] engine_0: COMMAND NOT FOUND. ERROR.
SBY  2:37:45 [demo2] engine_1: finished (returncode=127)
SBY  2:37:45 [demo2] engine_1: COMMAND NOT FOUND. ERROR.
SBY  2:37:45 [demo2] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  2:37:45 [demo2] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  2:37:45 [demo2] DONE (ERROR, rc=16)
make: *** [Makefile:59: test_demo2] Error 16

[jix]

Please run make run_tests or make from within the tests directory instead, make ci currently does requires a full OSS CAD Suite install. I'll look into documenting this and also into making the more standard make test do the same thing.

[programmerjake]

Please run make run_tests or make from within the tests directory instead,

aah. that also gives an error:

/tmp/sby$ make run_tests
...
cd unsorted && python3 /tmp/sby/sbysrc/sby.py -f stopfirst.sby
SBY  3:25:01 [stopfirst] Removing directory '/tmp/sby/tests/unsorted/stopfirst'.
SBY  3:25:01 [stopfirst] Writing 'stopfirst/src/test.sv'.
SBY  3:25:01 [stopfirst] engine_0: btor btormc
SBY  3:25:01 [stopfirst] base: starting process "cd stopfirst/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  3:25:01 [stopfirst] base: finished (returncode=0)
SBY  3:25:01 [stopfirst] btor: starting process "cd stopfirst/model; yosys -ql design_btor.log design_btor.ys"
SBY  3:25:01 [stopfirst] btor: finished (returncode=0)
SBY  3:25:01 [stopfirst] engine_0: starting process "cd stopfirst; btormc --stop-first 1 -v 1 -kmax 19 model/design_btor.btor"
SBY  3:25:01 [stopfirst] engine_0: [btor>mc] calling BMC on 2 properties from bound 0 up-to maximum bound k = 19
SBY  3:25:01 [stopfirst] engine_0: [btor>mc] bad state property 0 reachable at bound k = 0 SATISFIABLE
SBY  3:25:01 [stopfirst] engine_0_0: starting process "cd stopfirst ; btorsim -c --vcd engine_0/trace.vcd --hierarchical-symbols --info model/design_btor.info model/design_btor.btor engine_0/trace.wit"
SBY  3:25:01 [stopfirst] engine_0: [btor>mc] found 1 reachable and 0 unreachable bad state properties at bound k = 0
SBY  3:25:01 [stopfirst] engine_0: [btor>mc] deleting model checker: 1 inputs, 0 states, 2 bad, 0 constraints
SBY  3:25:01 [stopfirst] engine_0: finished (returncode=0)
SBY  3:25:01 [stopfirst] engine_0_0: bash: btorsim: command not found
SBY  3:25:01 [stopfirst] engine_0_0: finished (returncode=127)
SBY  3:25:01 [stopfirst] engine_0_0: COMMAND NOT FOUND. ERROR.
SBY  3:25:01 [stopfirst] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  3:25:01 [stopfirst] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  3:25:01 [stopfirst] DONE (ERROR, rc=16)
make[1]: *** [make/rules/test/unsorted/stopfirst.sby.mk:3: unsorted/stopfirst] Error 16
make[1]: Leaving directory '/tmp/sby/tests'
make: *** [Makefile:117: run_tests] Error 2

[jix]

Ah, I wasn't aware that the btor solvers can be installed without making btorsim available, on my system boolector/btormc pulled in btorsim via btor2tools as a dependency, I'll fix the (only recently added) detection code to also check for that. If you manually installed boolector, also note the comment on the btor2tools version mentioned in the installation instructions.

In case you only want to test a specific engine or solver you can also run make test_e_smtbmc or make test_s_yices from within the tests directory (see make help, again within the tests dir, for the supported filters).