v4.5.0: ASSERTION VIOLATION File: ../src/util/vector.h Line: 243

[ngilmore-grammatech]

Yes, I know this is in 2.5.0, and does not reproduce in 2.6.0 with this input file. Still, it may reproduce with some other input file.

The problem seems to be connected with the difference between debug and release builds. We've seen a few of these over the years, which is why I'm posting this, even though the version isn't the newest. The problem might still be lurking for different input.

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

Using ./configure -d and running z3 -smt x3.smt2, the results are:
sat
unsat
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 243
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

I did do a little debugging. Here's the backtrace:
#0 0x00007ffff732e035 in __GI_raise (sig=6)
at ../nptl/sysdeps/unix/sysv/linux/raise.c:64
#1 0x00007ffff733179b in __GI_abort () at abort.c:91
#2 0x000000000041b878 in vector<char, false, unsigned int>::operator[] (
this=0x194b1f0, idx=5245) at third-party/z3/src/util/vector.h:243
#3 0x0000000000ec2b84 in sat::solver::is_marked_lit (this=0x194a900, l=...)
at third-party/z3/src/sat/sat_solver.h:255
#4 0x0000000000ebc1ae in sat::solver::dyn_sub_res (this=0x194a900)
at third-party/z3/src/sat/sat_solver.cpp:2465
#5 0x0000000000eb99fe in sat::solver::resolve_conflict_core (this=0x194a900)
at third-party/z3/src/sat/sat_solver.cpp:1758
#6 0x0000000000eb926f in sat::solver::resolve_conflict (this=0x194a900)
at third-party/z3/src/sat/sat_solver.cpp:1637
#7 0x0000000000eb619f in sat::solver::propagate_and_backjump_step (
this=0x194a900, done=@0x7fffffffd73f: true)
at third-party/z3/src/sat/sat_solver.cpp:860
#8 0x0000000000eb60fc in sat::solver::bounded_search (this=0x194a900)
at third-party/z3/src/sat/sat_solver.cpp:840
#9 0x0000000000eb5b83 in sat::solver::check (this=0x194a900, num_lits=0,
lits=0x0, weights=0x0, max_weight=0)
at third-party/z3/src/sat/sat_solver.cpp:734
#10 0x00000000005e1112 in inc_sat_solver::check_sat (this=0x194a8e8, sz=0,
assumptions=0x194d300, weights=0x0, max_weight=0)
at third-party/z3/src/sat/sat_solver/inc_sat_solver.cpp:143
#11 0x00000000005e0ceb in inc_sat_solver::check_sat (this=0x194a8e8,
num_assumptions=0, assumptions=0x194d300)
at third-party/z3/src/sat/sat_solver/inc_sat_solver.cpp:109
#12 0x0000000000f7e5e9 in combined_solver::check_sat (this=0x194e1e8,
num_assumptions=0, assumptions=0x194d300)
at third-party/z3/src/solver/combined_solver.cpp:230
#13 0x0000000000d2cabf in cmd_context::check_sat (this=0x7fffffffe320,
num_assumptions=0, assumptions=0x194d300)
at third-party/z3/src/cmd_context/cmd_context.cpp:1371
#14 0x0000000000c72d98 in smt2::parser::parse_check_sat (this=0x7fffffffdaf0)
at third-party/z3/src/parsers/smt2/smt2parser.cpp:2176
#15 0x0000000000c74d56 in smt2::parser::parse_cmd (this=0x7fffffffdaf0)
at third-party/z3/src/parsers/smt2/smt2parser.cpp:2506
#16 0x0000000000c75dc0 in smt2::parser::operator() (this=0x7fffffffdaf0)
at third-party/z3/src/parsers/smt2/smt2parser.cpp:2661
#17 0x0000000000c663c1 in parse_smt2_commands (ctx=..., is=...,
interactive=false, ps=...)
at third-party/z3/src/parsers/smt2/smt2parser.cpp:2710
#18 0x0000000000406f06 in read_smtlib2_commands (
file_name=0x7fffffffebdf "x3.smt2")
at third-party/z3/src/shell/smtlib_frontend.cpp:130
#19 0x000000000041a5e9 in main (argc=3, argv=0x7fffffffe918)
at third-party/z3/src/shell/main.cpp:360

The basic problem is that doing the is_marked_lit(~l2) in sat_solver.cpp:2465 tried to access m_lit_mark with an index greater than size(). m_lit_mark appears to be the right size (2 X something else). And it was attempting to access an odd index, which is correct as the 'not' indexes are the odd ones.

The file has been attached as a .txt file, as .smt2 doesn't appear to be supported.
x3.txt

[NikolajBjorner]

Could you double check the attached file? I get answers "sat" "sat" and no crash.

[ngilmore-grammatech]

Sure, I can check. Here's starting from scratch:

wget https://github.com/Z3Prover/z3/archive/z3-4.5.0.tar.gz

tar xvf z3-4.5.0.tar.gz

mv z3-z3-4.5.0 z3-z3-4.5.0-debug
<because I also have a release version built and don't want to forget which is which>
cd z3-z3-4.5.0-debug
./configure -d
opt = -d, arg =
<various 'New Component' output>
<various 'Generating/Generated' output>

<various 'Copied' output>
<and here's the rest...
Testing ar...
Testing g++...
Testing gcc...
Testing floating point support...
Testing OpenMP...
Host platform: Linux
C++ Compiler: g++
C Compiler : gcc
Archive Tool: ar
Arithmetic: internal
OpenMP: True
Prefix: /usr
64-bit: True
FP math: SSE2-GCC
Python pkg dir: /usr/lib/python2.7/dist-packages
Python version: 2.7
Writing build/Makefile
Copied Z3Py example 'socrates.py' to 'build/python'
Copied Z3Py example 'all_interval_series.py' to 'build/python'
Copied Z3Py example 'example.py' to 'build/python'
Copied Z3Py example 'visitor.py' to 'build/python'
Makefile was successfully generated.
compilation mode: Debug
Type 'cd build; make' to build Z3
and that's the end of the output for ./configure -d>
cd build
g++ --version
<and the output:
g++ (Ubuntu/Linaro 4.6.3-1ubuntu5) 4.6.3
Copyright (C) 2011 Free Software Foundation, Inc.
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

make

wget https://github.com/Z3Prover/z3/files/1682078/x3.txt

mv x3.txt x3.smt2
./z3 -smt2 x3.smt2
<output ...
sat
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 243
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

OK, thanks. I wasn't using 4.5. It repros there, but not on 4.6. I ported the fix to the current branch. I will not be patching old releases though. The fix is to reset the probing cache when variables are gc'ed because the probing cache ends up with stale literals.

[ngilmore-grammatech]

Thanks for the fix. I didn't expect that you'd patch an old release. I figured the best I'd get would be a fix in the current branch that I might backport. Or we'd move forward to 4.6.0, if we could.

[NikolajBjorner]

You are free to backport fixes, but I hope there are better ways to spend efforts. The backport is similar to the changes cb68960