v4.6.0: ASSERTION VIOLATION File: ../src/sat/sat_integrity_checker.cpp Line: 197

[ngilmore-grammatech]

Another bug where the release version and debug version behave differently.

This one happens in 4.6.0 and 4.5.0.

File is attached.

Using ./configure, and running z3 -smt x.smt2, the results are:
unsat
unsat

Using ./configure -d and running z3 -smt x.smt2, the results are:
unsat
unsat
ASSERTION VIOLATION
File: ../src/sat/sat_integrity_checker.cpp
Line: 197
s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned()))
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

Here's a trace from gdb:
#0 0x00007ffff6cab330 in __read_nocancel ()
at ../sysdeps/unix/syscall-template.S:81
#1 0x00007ffff6c365b0 in _IO_new_file_underflow (
fp=0x7ffff6f7f640 <IO_2_1_stdin>) at fileops.c:613
#2 0x00007ffff6c3753e in __GI__IO_default_uflow (
fp=0x7ffff6f7f640 <IO_2_1_stdin>) at genops.c:435
#3 0x00007ffff6c2dace in _IO_getc (fp=0x7ffff6f7f640 <IO_2_1_stdin>)
at getc.c:39
#4 0x00007ffff774368d in __gnu_cxx::stdio_sync_filebuf<char, std::char_traits >::underflow() () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#5 0x00007ffff772e092 in std::istream::sentry::sentry(std::istream&, bool) ()
from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#6 0x00007ffff772f62b in std::basic_istream<char, std::char_traits >& std::operator>><char, std::char_traits >(std::basic_istream<char, std::char_traits >&, char&) () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#7 0x00000000016caeda in invoke_gdb () at ../src/util/debug.cpp:79
#8 0x00000000015477e9 in sat::integrity_checker::check_watches (
this=0x7fffffffe310) at ../src/sat/sat_integrity_checker.cpp:156
#9 0x0000000001547e20 in sat::integrity_checker::operator() (
this=0x7fffffffe310) at ../src/sat/sat_integrity_checker.cpp:235
#10 0x0000000001529429 in sat::solver::check_invariant (this=0x1f0b748)
at ../src/sat/sat_solver.cpp:2840
#11 0x000000000151a162 in sat::solver::~solver (this=0x1f0b748,
__in_chrg=) at ../src/sat/sat_solver.cpp:61
#12 0x000000000052f32c in inc_sat_solver::~inc_sat_solver (this=0x1f0b728,
__in_chrg=) at ../src/sat/sat_solver/inc_sat_solver.cpp:86
#13 0x0000000000494643 in deallocf<check_sat_result> (
file=0x172d7d0 "../src/solver/check_sat_result.h", line=47, ptr=0x1f0b728)
at ../src/util/memory_manager.h:83
#14 0x0000000000493c25 in check_sat_result::dec_ref (this=0x1f0b728)
at ../src/solver/check_sat_result.h:47
#15 0x0000000000495291 in ref::dec_ref (this=0x1f0dc80)
at ../src/util/ref.h:34
#16 0x00000000004946e0 in ref::~ref (this=0x1f0dc80,
__in_chrg=) at ../src/util/ref.h:55
#17 0x00000000010472dc in combined_solver::~combined_solver (this=0x1f0dc58,
__in_chrg=) at ../src/solver/combined_solver.cpp:44
#18 0x0000000000494643 in deallocf<check_sat_result> (
file=0x172d7d0 "../src/solver/check_sat_result.h", line=47, ptr=0x1f0dc58)
at ../src/util/memory_manager.h:83
#19 0x0000000000493c25 in check_sat_result::dec_ref (this=0x1f0dc58)
at ../src/solver/check_sat_result.h:47
#20 0x0000000000495291 in ref::dec_ref (this=0x7fffffffe780)
at ../src/util/ref.h:34
#21 0x0000000000494735 in ref::operator= (this=0x7fffffffe780, ptr=0x0)
at ../src/util/ref.h:81
#22 0x0000000000fa7622 in cmd_context::reset (this=0x7fffffffe530,
finalize=true) at ../src/cmd_context/cmd_context.cpp:1258
#23 0x0000000000fa24dc in cmd_context::~cmd_context (this=0x7fffffffe530,
__in_chrg=) at ../src/cmd_context/cmd_context.cpp:500
#24 0x000000000042dae3 in read_smtlib2_commands (
file_name=0x7fffffffed77 "/u1/ngilmore/18503.smt2")
at ../src/shell/smtlib_frontend.cpp:107
#25 0x000000000042ef18 in main (argc=3, argv=0x7fffffffeb28)
at ../src/shell/main.cpp:337

File attached as .txt because it won't attach as .smt2
x.txt

[NikolajBjorner]

I am not reproducing this so far. Is this seen on Ubuntu?

[ngilmore-grammatech]

My profuse apologies. Wrong file. Here's the failing one. (Again renamed to .txt from .smt2)

Also, I can't find it now, but I think I ran across something about problems buildign z3 with g++ 4.8.x? But I don't seem to remember where. So I also built 4.6.0 with g++ 4.9.4 (on a different system, though I also built with 4.8.4 ) and got the same result.

18503.txt

[ngilmore-grammatech]

And yes, on Ubuntu 14.04 LTS (both systems I built on).

[ngilmore-grammatech]

Thanks for the fix.