1

Closed

assertion violation: s.m_qhead == s.m_trail.size()

description

Version:
End of master branch built with Z3DEBUG=1 and _EXTERNAL_RELEASE=1, plus cherry-picked changes:
https://z3.codeplex.com/SourceControl/changeset/110fa0b7fb711418fe2be67f033e8ed70b354972
https://z3.codeplex.com/SourceControl/changeset/f4f1c63abb4a6fd0df908e376b0ab014bce3d9da

Reproduces independently of cherry picked changes, but does depend on _EXTERNAL_RELEASE being defined.
ASSERTION VIOLATION
File: ../src/sat/sat_asymm_branch.cpp
Line: 79
s.m_qhead == s.m_trail.size()
Problematic input:
(set-logic QF_BV)
(define-sort bv64 () (_ BitVec 64))
(declare-fun chartab_addr!56 () bv64)
(define-fun tmp!58 () bv64 (bvadd chartab_addr!56 #x0000000000000100))
(define-fun tmp!65 () Bool (bvule chartab_addr!56 tmp!58))
(assert tmp!65)
(declare-fun str_addr!12 () bv64)
(define-fun tmp!66 () Bool (bvult tmp!58 str_addr!12))
(assert tmp!66)
(declare-fun _param_1_addr!10 () bv64)
(declare-fun p_addr!31 () bv64)
(define-fun tmp!69 () Bool (bvult _param_1_addr!10 p_addr!31))
(assert tmp!69)
(define-sort bv32 () (_ BitVec 32))
(define-sort bv8 () (_ BitVec 8))
(declare-fun str_addr_12_D0_15_D0!50 () bv8)
(define-fun tmp!52 () bv32 ((_ zero_extend 24) str_addr_12_D0_15_D0!50))
(define-fun tmp!53 () Bool (bvsge tmp!52 #x00000080))
(define-fun tmp!55 () Bool (not tmp!53))
(assert tmp!55)
(define-fun tmp!59 () bv64 ((_ zero_extend 56) str_addr_12_D0_15_D0!50))
(define-fun tmp!60 () bv64 (bvadd chartab_addr!56 tmp!59))
(define-fun tmp!61 () Bool (bvult tmp!60 chartab_addr!56))
(assert tmp!61)
(check-sat)
stack:
#2  0x0000000000b2a416 in sat::asymm_branch::operator() (this=0x7fffffffc8b0, force=false) at third-party/z3/src/sat/sat_asymm_branch.cpp:79
#3  0x0000000000b0a22f in sat::solver::simplify_problem (this=0x7fffffffc418) at third-party/z3/src/sat/sat_solver.cpp:882
#4  0x0000000000b0963f in sat::solver::check (this=0x7fffffffc418) at third-party/z3/src/sat/sat_solver.cpp:698
#5  0x0000000000a17091 in sat_tactic::imp::operator() (this=0x7fffffffc400, g=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/sat/tactic/sat_tactic.cpp:70
#6  0x0000000000a1787d in sat_tactic::operator() (this=0x13bf778, g=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/sat/tactic/sat_tactic.cpp:174
#7  0x0000000000bdacf6 in cleanup_tactical::operator() (this=0x13bf7c8, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:1206
#8  0x0000000000bdb371 in cond_tactical::operator() (this=0x13c0f68, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:1303
#9  0x0000000000bd4dc6 in and_then_tactical::operator() (this=0x13c4948, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:176
#10 0x0000000000bd4dc6 in and_then_tactical::operator() (this=0x13c4988, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:176
#11 0x0000000000bdb371 in cond_tactical::operator() (this=0x13c6198, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:1303
#12 0x0000000000bdb335 in cond_tactical::operator() (this=0x13c6218, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:1301
#13 0x0000000000bd4dc6 in and_then_tactical::operator() (this=0x13c6268, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:176
#14 0x0000000000bd942a in unary_tactical::operator() (this=0x13c62a8, in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactical.cpp:989
#15 0x0000000000be7864 in exec (t=..., in=..., result=..., mc=..., pc=..., core=...) at third-party/z3/src/tactic/tactic.cpp:180
#16 0x0000000000be7ad8 in check_sat (t=..., g=..., md=..., pr=..., core=..., reason_unknown=...) at third-party/z3/src/tactic/tactic.cpp:202


(gdb) p s.m_qhead
$2 = 262
(gdb) p s.m_trail.size()
$3 = 265
Closed Jun 13, 2013 at 9:47 PM by leodemoura
Fixed in the unstable branch

comments

leodemoura wrote Jun 13, 2013 at 9:47 PM