1

Closed

assertion violation: is_marked_lit(m_lemma[0])

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
2c8b314a15ba
40b1137b30da


Triggered this when trying out the bvumul_noovfl construct. I don't know whether this issue will actually matter in practice, since z3 runs for so long before hitting it.
ASSERTION VIOLATION
File: third-party/z3/src/sat/sat_solver.cpp
Line: 1798
is_marked_lit(m_lemma[0])
Here is the input. Z3 runs for about 2 hours and 15 minutes before crashing.
(define-sort bv32 () (_ BitVec 32))
(declare-fun _param_2_addr_26_D0!28 () bv32)
(define-fun tmp!37 () Bool (= #x00000000 _param_2_addr_26_D0!28))
(define-fun tmp!38 () Bool (not tmp!37)) ; check for division by zero
(assert tmp!38)
(define-fun tmp!36 () bv32 (bvudiv #xffffffff _param_2_addr_26_D0!28)) ; 4294967295 / j
(declare-fun _param_1_addr_13_D0!15 () bv32)
(define-fun tmp!39 () Bool (bvult tmp!36 _param_1_addr_13_D0!15))
(define-fun tmp!41 () Bool (not tmp!39)) ; [control-point] 4294967295 / j < i
(assert tmp!41)
(define-fun tmp!43 () Bool (bvumul_noovfl _param_1_addr_13_D0!15 _param_2_addr_26_D0!28))
(define-fun tmp!44 () Bool (not tmp!43))
(assert tmp!44)
(check-sat)
Here is a variation that only takes 15 minutes to crash:
(define-sort bv32 () (_ BitVec 32))
(declare-fun _param_2_addr_26_D0!28 () bv32)
(define-fun tmp!40 () Bool (= #x00000000 _param_2_addr_26_D0!28))
(define-fun tmp!41 () Bool (not tmp!40)) ; check for division by zero
(assert tmp!41)
(declare-fun _param_1_addr_13_D0!15 () bv32)
(define-fun tmp!39 () bv32 (bvudiv _param_1_addr_13_D0!15 _param_2_addr_26_D0!28)) ; i / j
(define-fun tmp!49 () Bool (bvumul_noovfl tmp!39 _param_2_addr_26_D0!28))
(define-fun tmp!50 () Bool (not tmp!49))
(assert tmp!50)
(check-sat)
These examples correspond to checking for integer overflow in the multiplications pictured below.
void *my_calloc(unsigned i, unsigned j)
{
    if( 0xffffffffU / j < i )
        return;
    return malloc( i*j );
}

void *fifteen_minute_crash(unsigned i, unsigned j)
{
    return malloc( (i/j)*j );
}
A little off topic: Any encoding suggestions to improve z3's performance here? It's OK if the answer is "no" :).
Closed Jun 29, 2013 at 2:23 AM by leodemoura
Fixed in the unstable branch

comments

leodemoura wrote Jun 27, 2013 at 9:49 PM

The assertion violation has been fixed some time ago in the unstable branch.
Here is the fix:
https://z3.codeplex.com/SourceControl/changeset/d26f0e1c28e9784e5c931dc326cc300089d8d03b