izlatkin / HornLauncher

scripts and reports for executions seahorn and test generation
0 stars 0 forks source link

[openssl_simplified] TG doesn't generate any testcases #35

Open izlatkin opened 2 years ago

izlatkin commented 2 years ago

23 out of 26 benchmarks stoped working. SMT2 s3_clnt_1.cil-1.smt2.txt

there is no error in the log file

s3_clnt_3.cil-1.c
s3_srvr_14.cil.c
s3_srvr_12.cil.c
s3_clnt_1.cil-2.c
s3_srvr_10.cil.c
s3_srvr_6.cil-1.c
s3_clnt_3.cil-2.c
s3_clnt_1.cil-1.c
s3_srvr_11.cil.c
s3_srvr_13.cil.c
s3_srvr_8.cil.c
s3_srvr_6.cil-2.c
s3_clnt_2.cil-2.c
s3_srvr_4.cil.c
s3_clnt_3.cil-3.c
s3_srvr_1b.cil.c
s3_clnt_4.cil-1.c
s3_srvr_1.cil-1.c
s3_srvr_2.cil-2.c
s3_srvr_7.cil.c
s3_clnt_4.cil-2.c
s3_srvr_2.cil-1.c
s3_srvr_3.cil.c
grigoryfedyukovich commented 2 years ago

More details needed. When did they stop working?

izlatkin commented 2 years ago

for example, for s3_clnt_1.cil-2 TG stopped generating testcase_*.h after https://github.com/izlatkin/aeval/commit/fe97f18b7c8e6a58b19ef132b8b18c5fdcbb9346

commit fe97f18b7c8e6a58b19ef132b8b18c5fdcbb9346
Date:   Sat Oct 9 09:18:24 2021 -0400

    further tuning the invariant generator
izlatkin commented 2 years ago

@grigoryfedyukovich results haven't changed and are available http://192.168.122.120/) only 2 out of 26 benchmarks works