Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

TISSAT is reporting an error #29

Closed
benjaminbartsch opened this issue Aug 28, 2022 · 2 comments
Closed

TISSAT is reporting an error #29

benjaminbartsch opened this issue Aug 28, 2022 · 2 comments

Comments

@benjaminbartsch
Copy link

Hi,
while compiling kissat (Download from 28.08.2022, 14:20) under Windows under cygwin the following test did not run successfully:

User@DESKTOP-5UC7OJ9 ~/kissat-master
$ ./configure && make test
configure: default configuration (see '-h')
configure: new build directory 'build'
configure: assuming GCC version 11.3.0 uses C99 by default
configure: compiler 'gcc  -W -Wall -O3 -DNDEBUG'
configure: linker 'gcc' (no additional options)
configure: using default 'ar' (no cross compilation)
configure: no 'tissat' binary generated (without '--test')
configure: no 'libkissat.so' shared library generated (without '-shared')
configure: no 'kitten' binary generated (without '--kitten')
configure: linking src/makefile
make -C "/home/User/kissat-master/build" test
make[1]: Entering directory '/home/User/kissat-master/build'
gcc -W -Wall -O3 -DNDEBUG -c ../src/allocate.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/analyze.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/ands.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/arena.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/assign.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/averages.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/backbone.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/backtrack.c
../scripts/generate-build-header.sh > build.h
gcc -W -Wall -O3 -DNDEBUG -I../build -c ../src/build.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/bump.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/check.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/clause.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/collect.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/colors.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/compact.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/config.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/decide.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/deduce.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/definition.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/dense.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/dump.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/eliminate.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/equivalences.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/error.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/extend.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/file.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/flags.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/format.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/forward.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/gates.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/heap.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/ifthenelse.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/import.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/internal.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/kimits.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/kitten.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/learn.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/logging.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/minimize.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/mode.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/options.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/phases.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/print.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/probe.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/profile.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/promote.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/proof.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/propbeyond.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/propdense.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/proprobe.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/propsearch.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/queue.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/reduce.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/reluctant.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/rephase.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/report.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/resize.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/resolve.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/resources.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/restart.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/search.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/shrink.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/smooth.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/sort.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/stack.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/statistics.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/strengthen.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/substitute.c
../src/substitute.c: In function ‘kissat_substitute’:
../src/substitute.c:575:30: warning: array subscript 3 is above array bounds of ‘unsigned int[3]’ [-Warray-bounds]
  575 |                       c->lits[old_size - 1] = INVALID_LIT;
      |                       ~~~~~~~^~~~~~~~~~~~~~
In file included from ../src/internal.h:9,
                 from ../src/inlinevector.h:4,
                 from ../src/inline.h:4,
                 from ../src/substitute.c:3:
../src/clause.h:34:12: note: while referencing ‘lits’
   34 |   unsigned lits[3];
      |            ^~~~
gcc -W -Wall -O3 -DNDEBUG -c ../src/sweep.c
../src/sweep.c: In function ‘substitute_connected_clauses.isra’:
../src/sweep.c:1082:28: warning: array subscript 3 is above array bounds of ‘unsigned int[3]’ [-Warray-bounds]
 1082 |                     c->lits[old_size - 1] = INVALID_LIT;
      |                     ~~~~~~~^~~~~~~~~~~~~~
In file included from ../src/internal.h:9,
                 from ../src/inlinevector.h:4,
                 from ../src/inline.h:4,
                 from ../src/sweep.c:2:
../src/clause.h:34:12: note: while referencing ‘lits’
   34 |   unsigned lits[3];
      |            ^~~~
gcc -W -Wall -O3 -DNDEBUG -c ../src/terminate.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/trail.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/utilities.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/vector.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/vivify.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/walk.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/warmup.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/watch.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/weaken.c
ar rc libkissat.a allocate.o analyze.o ands.o arena.o assign.o averages.o backbone.o backtrack.o build.o bump.o check.o clause.o collect.o colors.o compact.o config.o decide.o deduce.o definition.o dense.o dump.o eliminate.o equivalences.o error.o extend.o file.o flags.o format.o forward.o gates.o heap.o ifthenelse.o import.o internal.o kimits.o kitten.o learn.o logging.o minimize.o mode.o options.o phases.o print.o probe.o profile.o promote.o proof.o propbeyond.o propdense.o proprobe.o propsearch.o queue.o reduce.o reluctant.o rephase.o report.o resize.o resolve.o resources.o restart.o search.o shrink.o smooth.o sort.o stack.o statistics.o strengthen.o substitute.o sweep.o terminate.o trail.o utilities.o vector.o vivify.o walk.o warmup.o watch.o weaken.o
gcc -W -Wall -O3 -DNDEBUG -c ../src/main.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/application.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/handle.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/parse.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/witness.c
gcc -o kissat main.o application.o handle.o parse.o witness.o libkissat.a -lm
gcc -W -Wall -O3 -DNDEBUG -I../build -c ../test/test.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testadd.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testallocate.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testapplication.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testarena.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testarray.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testbump.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testceil.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testcollect.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testconfig.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testcoverage.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testdivert.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testdump.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testendianness.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testerror.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testfile.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testformat.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testheap.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testinit.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testkitten.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testmain.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testmessages.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testoptions.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testparse.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testprove.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testqueue.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testrandom.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testrank.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testreferences.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testreluctant.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testscheduler.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testsizes.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testsolve.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testsort.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/teststack.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testterminate.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testusage.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testutilities.c
gcc -W -Wall -O3 -DNDEBUG -c ../test/testvector.c
gcc -o tissat test.o application.o handle.o parse.o witness.o testadd.o testallocate.o testapplication.o testarena.o testarray.o testbump.o testceil.o testcollect.o testconfig.o testcoverage.o testdivert.o testdump.o testendianness.o testerror.o testfile.o testformat.o testheap.o testinit.o testkitten.o testmain.o testmessages.o testoptions.o testparse.o testprove.o testqueue.o testrandom.o testrank.o testreferences.o testreluctant.o testscheduler.o testsizes.o testsolve.o testsort.o teststack.o testterminate.o testusage.o testutilities.o testvector.o libkissat.a -lm
./tissat
TISSAT Tester for KISSAT

Copyright (c) 2021-2022 Armin Biere University of Freiburg
Copyright (c) 2019-2021 Armin Biere Johannes Kepler University Linz

Version 3.0.0 unknown
gcc (GCC) 11.3.0 -W -Wall -O3 -DNDEBUG
Sun, Aug 28, 2022 2:18:54 PM CYGWIN_NT-10.0-22000 DESKTOP-5UC7OJ9 3.3.5-341.x86_64 x86_64

Use '-h' to print usage (i.e., how to use patterns).
Changed to '/home/User/kissat-master/build' directory.
Parallel execution using at most 32 processes (by default).
Job execution progress reporting disabled (enable with '-p').

Found '../test' directory (running test cases that need '../test' too).
Did not find 'drabt' executable.
Did not find 'drat-trim' executable.

Install either 'drat-trim' or 'drabt' to check proofs too!

Found 'bzip2' executable for testing compression.
Found 'gzip' executable for testing compression.
Found 'lzma' executable for testing compression.
Found 'xz' executable for testing compression.
Did not find '7z' executable for testing compression.

Scheduled 4 jobs through 'tissat_schedule_error'.
Scheduled 1 jobs through 'tissat_schedule_utilities'.
Scheduled 1 jobs through 'tissat_schedule_endianness'.
Scheduled 3 jobs through 'tissat_schedule_ceil'.
Scheduled 1 jobs through 'tissat_schedule_format'.
Scheduled 2 jobs through 'tissat_schedule_references'.
Scheduled 1 jobs through 'tissat_schedule_reluctant'.
Scheduled 2 jobs through 'tissat_schedule_random'.
Scheduled 1 jobs through 'tissat_schedule_queue'.
Scheduled 3 jobs through 'tissat_schedule_allocate'.
Scheduled 1 jobs through 'tissat_schedule_array'.
Scheduled 2 jobs through 'tissat_schedule_stack'.
Scheduled 4 jobs through 'tissat_schedule_arena'.
Scheduled 3 jobs through 'tissat_schedule_heap'.
Scheduled 2 jobs through 'tissat_schedule_vector'.
Scheduled 2 jobs through 'tissat_schedule_rank'.
Scheduled 2 jobs through 'tissat_schedule_sort'.
Scheduled 1 jobs through 'tissat_schedule_bump'.
Scheduled 4 jobs through 'tissat_schedule_options'.
Scheduled 2 jobs through 'tissat_schedule_config'.
Scheduled 5 jobs through 'tissat_schedule_init'.
Scheduled 1 jobs through 'tissat_schedule_add'.
Scheduled 6 jobs through 'tissat_schedule_file'.
Scheduled 2 jobs through 'tissat_schedule_parse'.
Scheduled 44 jobs through 'tissat_schedule_usage'.
Scheduled 6 jobs through 'tissat_schedule_main'.
Scheduled 1 jobs through 'tissat_schedule_collect'.
Scheduled 2 jobs through 'tissat_schedule_kitten'.
Scheduled 414 jobs through 'tissat_schedule_solve'.
Scheduled 45 jobs through 'tissat_schedule_coverage'.
Scheduled 0 jobs through 'tissat_schedule_terminate'.

Running 568 jobs in parallel using up to 32 processes.
tissat: fatal error: 'kissat --walkinitially --conflicts=3000 --probeinit=0 --eliminateinit=0 ../test/cnf/hard.cnf --profile=4' returns '1' and not '0'
tissat: fatal error: 'kissat ../test/cnf/hard.cnf --walkinitially -v -v -v --colors --conflicts=1e4' returns '1' and not '0'
Stack trace:
Frame        Function    Args
000FFFFBE90  00180062277 (000FFFFC098, 00000000002, 00000000002, 000FFFFDE50)
00000000000  001800642F5 (000FFFFC840, 00000000000, 00000000180, 00000000000)
000FFFFC5A0  00180133018 (00180143837, 0018026A7A0, 00000000004, 00000000002)
00000000041  0018012E64B (00180156060, 00000000000, 00000000000, 00000000000)
00000000001  0018012EA55 (000FFFFC998, 0010045F050, 00800068A60, 0080006F590)
00000000001  00180215498 (00180230EE8, 0010045F074, 000FFFFC9B0, 0010045F037)
00000000001  00100410799 (00800068A60, 00000000001, 00000000000, 0010045F030)
00000000001  00100404B30 (00800068A60, 00000000002, 00000000000, 00000000D90)
0010046760D  0010041A8EC (000FFFFCABC, 00000000020, 00000000000, 000FFFFD680)
0010046760D  0010041B15F (00000000000, 0010045CC89, 000FFFFCC80, 00000000000)
001004F53C4  0010045A4EF (00180049B11, 00180048A70, 00000000002, 00180325FC0)
000FFFFCD30  00180049B7D (00000000000, 00000000000, 00000000000, 00000000000)
000FFFFFFF0  00180047746 (00000000000, 00000000000, 00000000000, 00000000000)
000FFFFFFF0  001800477F4 (00000000000, 00000000000, 00000000000, 00000000000)
End of stack trace
                  tissat: unexpected signal: Caught signal '6' (SIGABRT) in application 'kissat ../test/cnf/hard.cnf --walkinitially -v -v -v --colors --conflicts=1e4'
tissat: fatal error: 'kissat --decisions=10 ../test/cnf/hard.cnf --no-reduce' returns '1' and not '0'
Stack trace:
Frame        Function    Args
000FFFFBE90  00180062277 (000FFFFC098, 00000000002, 00000000002, 000FFFFDE50)
00000000000  001800642F5 (000FFFFC840, 00000000000, 0000000017C, 00000000000)
000FFFFC5A0  00180133018 (00180143837, 0018026A7A0, 00000000002, 00000000002)
00000000041  0018012E64B (00180156060, 00000000000, 00000000000, 00000000000)
00000000001  0018012EA55 (000FFFFC998, 0010045F050, 00800068AB0, 0080006F510)
00000000001  00180215498 (00180230EE8, 0010045F074, 000FFFFC9B0, 0010045F037)
00000000001  00100410799 (00800068AB0, 00000000001, 00000000000, 0010045F030)
00000000001  00100404B30 (00800068AB0, 00000000002, 00000000000, 00000000D91)
0010046760D  0010041A8EC (000FFFFCABC, 00000000020, 00000000000, 000FFFFD680)
0010046760D  0010041B15F (00000000000, 0010045CC89, 000FFFFCC80, 00000000000)
001004F53C4  0010045A4EF (00180049B11, 00180048A70, 00000000002, 00180325FC0)
000FFFFCD30  00180049B7D (00000000000, 00000000000, 00000000000, 00000000000)
000FFFFFFF0  00180047746 (00000000000, 00000000000, 00000000000, 00000000000)
000FFFFFFF0  001800477F4 (00000000000, 00000000000, 00000000000, 00000000000)
End of stack trace
                  make[1]: *** [makefile:31: test] Error 1
make[1]: Leaving directory '/home/User/kissat-master/build'
make: *** [makefile:16: test] Error 2
@benjaminbartsch
Copy link
Author

benjaminbartsch commented Aug 28, 2022 •
edited
Loading

... under Linux Mint the error does not happen. So it seems, that somehow cygwin+gcc does not compile the source code correctly.

Context: I am using kissat under windows inside a JAVA programm (it opens a Process/Shell in the background), which creates CNF data and sends it via pipes to kissat. This also crashed (using the exe-file from cygwin) and reports, that kissat did close the pipe too early.

But using this executable #7 everything works fine.

@benjaminbartsch
Copy link
Author

benjaminbartsch commented Aug 30, 2022 •
edited
Loading

I am closing this issue, since if compiled like #7 its working.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@benjaminbartsch