[17:06:26:538451] docker exec unruffled_lederberg bash -c cd /app/eq1; ../smt_run.sh /app/eq1/eq1.c /app/eq1/eq1.smt2 [17:06:26:757600] docker exec unruffled_lederberg bash -c cd /app/eq1; ../smt_run.sh /app/eq1/eq1.c /app/eq1/eq1.smt2 0 b'' b"/app/eq1/eq1.c:4:113: warning: unknown attribute '__leaf__' ignored [-Wunknown-attributes] extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); ^ 1 warning generated. " [17:06:26:758446] /home/fmfsu/aeval/build/tools/tg/tg --inv-mode 2 --phase-prop --no-term --keys 15289,15359,3683,2501 eq1.smt2 [17:06:33:123080] /home/fmfsu/aeval/build/tools/tg/tg --inv-mode 2 --phase-prop --no-term --keys 15289,15359,3683,2501 eq1.smt2 0 b'Incomplete (define-fun main@_.05 ((_FH_0 Int)(_FH_1 Int)(_FH_2 Int)(_FH_3 Int)(_FH_4 Int)) Bool (and (= _FH_4 0) (= (+ _FH_0 _FH_2 (* (- 1) _FH_1) (* (- 1) _FH_3)) 0) (= (+ _FH_0 _FH_3 (* (- 1) _FH_1) (* (- 1) _FH_2)) 0) (= (+ _FH_0 _FH_4 (* (- 1) _FH_1)) 0) (= (+ _FH_0 (* (- 1) _FH_1) (* (- 1) _FH_4)) 0) (= (+ _FH_0 (* (- 1) _FH_1)) 0) (= (+ _FH_2 _FH_4 (* (- 1) _FH_3)) 0) (= (+ _FH_2 (* (- 1) _FH_3) (* (- 1) _FH_4)) 0) (= (+ _FH_2 (* (- 1) _FH_3)) 0) (= (+ _FH_1 _FH_3 (* (- 1) _FH_2) (* (- 1) _FH_0)) 0) (= (+ _FH_1 _FH_2 (* (- 1) _FH_3) (* (- 1) _FH_0)) 0) (= (+ _FH_1 _FH_4 (* (- 1) _FH_0)) 0) (= (+ _FH_1 (* (- 1) _FH_4) (* (- 1) _FH_0)) 0) (= (+ _FH_1 (* (- 1) _FH_0)) 0) (= (+ _FH_3 _FH_4 (* (- 1) _FH_2)) 0) (= (+ _FH_3 (* (- 1) _FH_2) (* (- 1) _FH_4)) 0) (= (+ _FH_3 (* (- 1) _FH_2)) 0) (= (+ _FH_0 (- _FH_1)) 0) (= (+ _FH_2 (- _FH_3)) 0))) unknown ======== Propagating invariants to all CHCs ====== Incomplete (define-fun verifier.error ((_FH_0 Bool)(_FH_1 Bool)(_FH_2 Bool)) Bool (or (and (not _FH_0) (not _FH_1) (not _FH_2)) (and _FH_1 _FH_2 (not _FH_0)) (and _FH_0 _FH_2 (not _FH_1)) (and _FH_0 _FH_1 _FH_2))) (define-fun main@_loop.bound () Bool true) (define-fun main@empty.loop ((_FH_0 Int)(_FH_1 Int)(_FH_2 Int)) Bool (= 0 _FH_0)) (define-fun main@_.05 ((_FH_0 Int)(_FH_1 Int)(_FH_2 Int)(_FH_3 Int)(_FH_4 Int)) Bool (and (= _FH_4 0) (= (+ _FH_0 _FH_2 (* (- 1) _FH_1) (* (- 1) _FH_3)) 0) (= (+ _FH_0 _FH_3 (* (- 1) _FH_1) (* (- 1) _FH_2)) 0) (= (+ _FH_0 _FH_4 (* (- 1) _FH_1)) 0) (= (+ _FH_0 (* (- 1) _FH_1) (* (- 1) _FH_4)) 0) (= (+ _FH_0 (* (- 1) _FH_1)) 0) (= (+ _FH_2 _FH_4 (* (- 1) _FH_3)) 0) (= (+ _FH_2 (* (- 1) _FH_3) (* (- 1) _FH_4)) 0) (= (+ _FH_2 (* (- 1) _FH_3)) 0) (= (+ _FH_1 _FH_3 (* (- 1) _FH_2) (* (- 1) _FH_0)) 0) (= (+ _FH_1 _FH_2 (* (- 1) _FH_3) (* (- 1) _FH_0)) 0) (= (+ _FH_1 _FH_4 (* (- 1) _FH_0)) 0) (= (+ _FH_1 (* (- 1) _FH_4) (* (- 1) _FH_0)) 0) (= (+ _FH_1 (* (- 1) _FH_0)) 0) (= (+ _FH_3 _FH_4 (* (- 1) _FH_2)) 0) (= (+ _FH_3 (* (- 1) _FH_2) (* (- 1) _FH_4)) 0) (= (+ _FH_3 (* (- 1) _FH_2)) 0) (= (+ _FH_0 (- _FH_1)) 0) (= (+ _FH_2 (- _FH_3)) 0))) (define-fun main@_22 ((_FH_0 Int)(_FH_1 Int)(_FH_2 Int)(_FH_3 Int)) Bool (and (= (+ _FH_0 (* (- 1) _FH_0)) 0) (= (+ _FH_2 (* (- 1) _FH_2)) 0) (= (+ _FH_0 _FH_2 (* (- 1) _FH_2) (* (- 1) _FH_0)) 0) (= (+ _FH_0 (- _FH_1)) 0) (= (+ _FH_2 (- _FH_3)) 0))) (define-fun main@_call3 ((_FH_0 Int)(_FH_1 Int)(_FH_2 Int)(_FH_3 Int)(_FH_4 Int)) Bool (and (= _FH_4 0) (= (+ _FH_0 (- _FH_1)) 0) (= (+ _FH_2 (- _FH_3)) 0))) (define-fun main@_18 ((_FH_0 Int)(_FH_1 Int)(_FH_2 Int)(_FH_3 Int)(_FH_4 Int)) Bool (and (= _FH_4 0) (= (+ _FH_0 (- _FH_1)) 0) (= (+ _FH_3 (- _FH_2)) 0))) (define-fun main@_15 ((_FH_0 Int)(_FH_1 Int)(_FH_2 Int)(_FH_3 Int)(_FH_4 Int)) Bool (and (= _FH_4 0) (= (+ _FH_0 (- _FH_1)) 0) (= (+ _FH_2 (- _FH_3)) 0))) (define-fun main@_.16 ((_FH_0 Int)(_FH_1 Int)(_FH_2 Int)(_FH_3 Int)(_FH_4 Int)) Bool (or (and (= _FH_4 0) (= (+ _FH_0 (- _FH_3)) 0) (= (+ _FH_2 (- _FH_1)) 0)) (and (= _FH_4 0) (= (+ _FH_0 (- _FH_3)) 0) (= (+ _FH_1 (- _FH_2)) 0)))) (define-fun main@empty.loop.body ((_FH_0 Int)(_FH_1 Int)(_FH_2 Int)) Bool true) new iter with cur_bnd = 1 exploring traces (0) of length 1; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 exploring traces (0) of length 1; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 exploring traces (0) of length 1; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 exploring traces (0) of length 1; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 new iter with cur_bnd = 2 exploring traces (0) of length 2; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 exploring traces (0) of length 2; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 exploring traces (0) of length 2; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 exploring traces (0) of length 2; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 new iter with cur_bnd = 3 exploring traces (0) of length 3; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 exploring traces (0) of length 3; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 exploring traces (0) of length 3; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 exploring traces (0) of length 3; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 new iter with cur_bnd = 4 exploring traces (1) of length 4; # of todos = 4 -> actually explored: 1, |unsat prefs| = 0 exploring traces (1) of length 4; # of todos = 4 -> actually explored: 1, |unsat prefs| = 0 exploring traces (0) of length 4; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 exploring traces (0) of length 4; # of todos = 4 -> actually explored: 0, |unsat prefs| = 0 new iter with cur_bnd = 5 exploring traces (1) of length 5; # of todos = 2 -> actually explored: 1, |unsat prefs| = 0 exploring traces (1) of length 5; # of todos = 2 -> actually explored: 1, |unsat prefs| = 0 Done with TG ' b'' [17:06:33:128516] rm -rf main.gc* main.o coverage.info test-coverage generated-coverage [17:06:33:132255] rm -rf main.gc* main.o coverage.info test-coverage generated-coverage 0 b'' b'' [17:06:33:132521] gcc-7 -pthread -O0 --coverage main.c -o test-coverage [17:06:33:185497] gcc-7 -pthread -O0 --coverage main.c -o test-coverage 0 b'' b'main.c: In function \xe2\x80\x98main\xe2\x80\x99: main.c:34:44: warning: passing argument 3 of \xe2\x80\x98pthread_create\xe2\x80\x99 from incompatible pointer type [-Wincompatible-pointer-types] pthread_t tid; pthread_create(&tid, 0, main_oririnal, 0); ^~~~~~~~~~~~~ In file included from main.c:1:0: /usr/include/pthread.h:234:12: note: expected \xe2\x80\x98void * (*)(void *)\xe2\x80\x99 but argument is of type \xe2\x80\x98int (*)(void)\xe2\x80\x99 extern int pthread_create (pthread_t *__restrict __newthread, ^~~~~~~~~~~~~~ main.c:35:115: warning: implicit declaration of function \xe2\x80\x98pthread_kill\xe2\x80\x99; did you mean \xe2\x80\x98pthread_self\xe2\x80\x99? [-Wimplicit-function-declaration] time_t start = time(0); time_t seconds = 10; time_t endwait = start + seconds; while ((start < endwait) & (pthread_kill(tid, 0) == 0)){ sleep(1); start = time(0); } ^~~~~~~~~~~~ pthread_self main.c:36:26: warning: implicit declaration of function \xe2\x80\x98printf\xe2\x80\x99 [-Wimplicit-function-declaration] pthread_cancel(tid); printf("timeout termination "); return 0; } ^~~~~~ main.c:36:26: warning: incompatible implicit declaration of built-in function \xe2\x80\x98printf\xe2\x80\x99 main.c:36:26: note: include \xe2\x80\x98\xe2\x80\x99 or provide a declaration of \xe2\x80\x98printf\xe2\x80\x99 In file included from main.c:5:0: testgen.h: In function \xe2\x80\x98__assert_fail\xe2\x80\x99: testgen.h:2:1: warning: \xe2\x80\x98noreturn\xe2\x80\x99 function does return void __assert_fail(const char * a, const char * b, unsigned int c, const char * d) {}; ^~~~ ' [17:06:33:185773] ./test-coverage [17:06:34:188595] ./test-coverage 0 b'timeout termination ' b'' [17:06:34:188880] lcov --capture --rc lcov_branch_coverage=1 --directory . --config-file ../../lcovrc --output coverage.info [17:06:34:299416] lcov --capture --rc lcov_branch_coverage=1 --directory . --config-file ../../lcovrc --output coverage.info 0 b'Capturing coverage data from . Found gcov version: 7.5.0 Scanning . for .gcda files ... Found 1 data files in . Processing main.gcda Finished .info-file creation ' b'' [17:06:34:299703] rm -rf /tmp/coverage/ [17:06:34:303422] rm -rf /tmp/coverage/ 0 b'' b'' [17:06:34:303689] genhtml --branch-coverage --output ./generated-coverage/ coverage.info [17:06:34:375700] genhtml --branch-coverage --output ./generated-coverage/ coverage.info 0 b'Reading data file coverage.info Found 2 entries. Found common filename prefix "/home/fmfsu/PyCharm/sandbox/eq1" Writing .css and .png files. Generating output. Processing file 1/main.c Processing file 1/testgen.h Writing directory view page. Overall coverage rate: lines......: 64.9% (24 of 37 lines) functions..: 66.7% (6 of 9 functions) branches...: 45.0% (9 of 20 branches) ' b'' [17:06:34:380762] rm -rf main.gc* main.o coverage.info test-coverage generated-coverage [17:06:34:384488] rm -rf main.gc* main.o coverage.info test-coverage generated-coverage 0 b'' b'' [17:06:34:384756] gcc-7 -pthread -O0 --coverage main.c -o test-coverage [17:06:34:437489] gcc-7 -pthread -O0 --coverage main.c -o test-coverage 0 b'' b'main.c: In function \xe2\x80\x98main\xe2\x80\x99: main.c:34:44: warning: passing argument 3 of \xe2\x80\x98pthread_create\xe2\x80\x99 from incompatible pointer type [-Wincompatible-pointer-types] pthread_t tid; pthread_create(&tid, 0, main_oririnal, 0); ^~~~~~~~~~~~~ In file included from main.c:1:0: /usr/include/pthread.h:234:12: note: expected \xe2\x80\x98void * (*)(void *)\xe2\x80\x99 but argument is of type \xe2\x80\x98int (*)(void)\xe2\x80\x99 extern int pthread_create (pthread_t *__restrict __newthread, ^~~~~~~~~~~~~~ main.c:35:115: warning: implicit declaration of function \xe2\x80\x98pthread_kill\xe2\x80\x99; did you mean \xe2\x80\x98pthread_self\xe2\x80\x99? [-Wimplicit-function-declaration] time_t start = time(0); time_t seconds = 10; time_t endwait = start + seconds; while ((start < endwait) & (pthread_kill(tid, 0) == 0)){ sleep(1); start = time(0); } ^~~~~~~~~~~~ pthread_self main.c:36:26: warning: implicit declaration of function \xe2\x80\x98printf\xe2\x80\x99 [-Wimplicit-function-declaration] pthread_cancel(tid); printf("timeout termination "); return 0; } ^~~~~~ main.c:36:26: warning: incompatible implicit declaration of built-in function \xe2\x80\x98printf\xe2\x80\x99 main.c:36:26: note: include \xe2\x80\x98\xe2\x80\x99 or provide a declaration of \xe2\x80\x98printf\xe2\x80\x99 In file included from main.c:5:0: testgen.h: In function \xe2\x80\x98__assert_fail\xe2\x80\x99: testgen.h:2:1: warning: \xe2\x80\x98noreturn\xe2\x80\x99 function does return void __assert_fail(const char * a, const char * b, unsigned int c, const char * d) {}; ^~~~ ' [17:06:34:437799] ./test-coverage [17:06:44:442400] ./test-coverage 0 b'timeout termination ' b'' [17:06:44:442706] lcov --capture --rc lcov_branch_coverage=1 --directory . --config-file ../../lcovrc --output coverage.info [17:06:44:553037] lcov --capture --rc lcov_branch_coverage=1 --directory . --config-file ../../lcovrc --output coverage.info 0 b'Capturing coverage data from . Found gcov version: 7.5.0 Scanning . for .gcda files ... Found 1 data files in . Processing main.gcda Finished .info-file creation ' b'' [17:06:44:553342] rm -rf /tmp/coverage/ [17:06:44:557046] rm -rf /tmp/coverage/ 0 b'' b'' [17:06:44:557310] genhtml --branch-coverage --output ./generated-coverage/ coverage.info [17:06:44:629848] genhtml --branch-coverage --output ./generated-coverage/ coverage.info 0 b'Reading data file coverage.info Found 2 entries. Found common filename prefix "/home/fmfsu/PyCharm/sandbox/eq1" Writing .css and .png files. Generating output. Processing file 2/main.c Processing file 2/testgen.h Writing directory view page. Overall coverage rate: lines......: 67.6% (25 of 37 lines) functions..: 66.7% (6 of 9 functions) branches...: 45.0% (9 of 20 branches) ' b'' [17:06:44:634917] rm -rf main.gc* main.o coverage.info test-coverage generated-coverage [17:06:44:638629] rm -rf main.gc* main.o coverage.info test-coverage generated-coverage 0 b'' b'' [17:06:44:638896] gcc-7 -pthread -O0 --coverage main.c -o test-coverage [17:06:44:691691] gcc-7 -pthread -O0 --coverage main.c -o test-coverage 0 b'' b'main.c: In function \xe2\x80\x98main\xe2\x80\x99: main.c:34:44: warning: passing argument 3 of \xe2\x80\x98pthread_create\xe2\x80\x99 from incompatible pointer type [-Wincompatible-pointer-types] pthread_t tid; pthread_create(&tid, 0, main_oririnal, 0); ^~~~~~~~~~~~~ In file included from main.c:1:0: /usr/include/pthread.h:234:12: note: expected \xe2\x80\x98void * (*)(void *)\xe2\x80\x99 but argument is of type \xe2\x80\x98int (*)(void)\xe2\x80\x99 extern int pthread_create (pthread_t *__restrict __newthread, ^~~~~~~~~~~~~~ main.c:35:115: warning: implicit declaration of function \xe2\x80\x98pthread_kill\xe2\x80\x99; did you mean \xe2\x80\x98pthread_self\xe2\x80\x99? [-Wimplicit-function-declaration] time_t start = time(0); time_t seconds = 10; time_t endwait = start + seconds; while ((start < endwait) & (pthread_kill(tid, 0) == 0)){ sleep(1); start = time(0); } ^~~~~~~~~~~~ pthread_self main.c:36:26: warning: implicit declaration of function \xe2\x80\x98printf\xe2\x80\x99 [-Wimplicit-function-declaration] pthread_cancel(tid); printf("timeout termination "); return 0; } ^~~~~~ main.c:36:26: warning: incompatible implicit declaration of built-in function \xe2\x80\x98printf\xe2\x80\x99 main.c:36:26: note: include \xe2\x80\x98\xe2\x80\x99 or provide a declaration of \xe2\x80\x98printf\xe2\x80\x99 In file included from main.c:5:0: testgen.h: In function \xe2\x80\x98__assert_fail\xe2\x80\x99: testgen.h:2:1: warning: \xe2\x80\x98noreturn\xe2\x80\x99 function does return void __assert_fail(const char * a, const char * b, unsigned int c, const char * d) {}; ^~~~ ' [17:06:44:691999] ./test-coverage [17:06:54:696588] ./test-coverage 0 b'timeout termination ' b'' [17:06:54:696892] lcov --capture --rc lcov_branch_coverage=1 --directory . --config-file ../../lcovrc --output coverage.info [17:06:54:806641] lcov --capture --rc lcov_branch_coverage=1 --directory . --config-file ../../lcovrc --output coverage.info 0 b'Capturing coverage data from . Found gcov version: 7.5.0 Scanning . for .gcda files ... Found 1 data files in . Processing main.gcda Finished .info-file creation ' b'' [17:06:54:806931] rm -rf /tmp/coverage/ [17:06:54:810630] rm -rf /tmp/coverage/ 0 b'' b'' [17:06:54:810896] genhtml --branch-coverage --output ./generated-coverage/ coverage.info [17:06:54:883500] genhtml --branch-coverage --output ./generated-coverage/ coverage.info 0 b'Reading data file coverage.info Found 2 entries. Found common filename prefix "/home/fmfsu/PyCharm/sandbox/eq1" Writing .css and .png files. Generating output. Processing file 3/testgen.h Processing file 3/main.c Writing directory view page. Overall coverage rate: lines......: 73.0% (27 of 37 lines) functions..: 66.7% (6 of 9 functions) branches...: 55.0% (11 of 20 branches) ' b'' [17:06:54:888570] rm -rf main.gc* main.o coverage.info test-coverage generated-coverage [17:06:54:892295] rm -rf main.gc* main.o coverage.info test-coverage generated-coverage 0 b'' b'' [17:06:54:892563] gcc-7 -pthread -O0 --coverage main.c -o test-coverage [17:06:54:945460] gcc-7 -pthread -O0 --coverage main.c -o test-coverage 0 b'' b'main.c: In function \xe2\x80\x98main\xe2\x80\x99: main.c:34:44: warning: passing argument 3 of \xe2\x80\x98pthread_create\xe2\x80\x99 from incompatible pointer type [-Wincompatible-pointer-types] pthread_t tid; pthread_create(&tid, 0, main_oririnal, 0); ^~~~~~~~~~~~~ In file included from main.c:1:0: /usr/include/pthread.h:234:12: note: expected \xe2\x80\x98void * (*)(void *)\xe2\x80\x99 but argument is of type \xe2\x80\x98int (*)(void)\xe2\x80\x99 extern int pthread_create (pthread_t *__restrict __newthread, ^~~~~~~~~~~~~~ main.c:35:115: warning: implicit declaration of function \xe2\x80\x98pthread_kill\xe2\x80\x99; did you mean \xe2\x80\x98pthread_self\xe2\x80\x99? [-Wimplicit-function-declaration] time_t start = time(0); time_t seconds = 10; time_t endwait = start + seconds; while ((start < endwait) & (pthread_kill(tid, 0) == 0)){ sleep(1); start = time(0); } ^~~~~~~~~~~~ pthread_self main.c:36:26: warning: implicit declaration of function \xe2\x80\x98printf\xe2\x80\x99 [-Wimplicit-function-declaration] pthread_cancel(tid); printf("timeout termination "); return 0; } ^~~~~~ main.c:36:26: warning: incompatible implicit declaration of built-in function \xe2\x80\x98printf\xe2\x80\x99 main.c:36:26: note: include \xe2\x80\x98\xe2\x80\x99 or provide a declaration of \xe2\x80\x98printf\xe2\x80\x99 In file included from main.c:5:0: testgen.h: In function \xe2\x80\x98__assert_fail\xe2\x80\x99: testgen.h:2:1: warning: \xe2\x80\x98noreturn\xe2\x80\x99 function does return void __assert_fail(const char * a, const char * b, unsigned int c, const char * d) {}; ^~~~ ' [17:06:54:945770] ./test-coverage [17:07:04:950371] ./test-coverage 0 b'timeout termination ' b'' [17:07:04:950675] lcov --capture --rc lcov_branch_coverage=1 --directory . --config-file ../../lcovrc --output coverage.info [17:07:05:060843] lcov --capture --rc lcov_branch_coverage=1 --directory . --config-file ../../lcovrc --output coverage.info 0 b'Capturing coverage data from . Found gcov version: 7.5.0 Scanning . for .gcda files ... Found 1 data files in . Processing main.gcda Finished .info-file creation ' b'' [17:07:05:061131] rm -rf /tmp/coverage/ [17:07:05:064870] rm -rf /tmp/coverage/ 0 b'' b'' [17:07:05:065135] genhtml --branch-coverage --output ./generated-coverage/ coverage.info [17:07:05:137418] genhtml --branch-coverage --output ./generated-coverage/ coverage.info 0 b'Reading data file coverage.info Found 2 entries. Found common filename prefix "/home/fmfsu/PyCharm/sandbox/eq1" Writing .css and .png files. Generating output. Processing file 4/main.c Processing file 4/testgen.h Writing directory view page. Overall coverage rate: lines......: 70.3% (26 of 37 lines) functions..: 66.7% (6 of 9 functions) branches...: 50.0% (10 of 20 branches) ' b'' [17:07:05:209087] total time: 38.72924208641052 seconds