Issues in arithmetic and string logics

[rainoftime]

heap-use-after-free at ast.h:506 (arith.bounded_expansion, qe_rec)
z3 commit 48d4d8d

(set-logic ALIA)
(set-option :smt.arith.bounded_expansion true)
(declare-const i7 Int)
(assert (exists ((q57 Int) (q58 Int)) (distinct q58 (mod i7 55))))
(assert (not (exists ((q61 Int)) (= 309 q61))))
(check-sat-using qe_rec) 

==69543==ERROR: AddressSanitizer: heap-use-after-free on address 0x6070000d98f4 at pc 0x000000468101 bp 0x7fff12614660 sp 0x7fff12614650
READ of size 4 at 0x6070000d98f4 thread T0
    #0 0x468100 in ast::hash() const ../src/ast/ast.h:506
    #1 0x5d2ec9 in obj_map<expr, expr*>::key_data::hash() const ../src/util/obj_hashtable.h:78
    #2 0x5d22a1 in obj_map<expr, expr*>::obj_map_entry::get_hash() const ../src/util/obj_hashtable.h:87
    #3 0x5d1fb7 in core_hashtable<obj_map<expr, expr*>::obj_map_entry, obj_hash<obj_map<expr, expr*>::key_data>, default_eq<obj_map<expr, expr*>::key_data> >::find_core(obj_map<expr, expr*>::key_data cons
t&) const ../src/util/hashtable.h:517
    #4 0x5d06c4 in obj_map<expr, expr*>::find_core(expr*) const ../src/util/obj_hashtable.h:158
    #5 0x68b724 in obj_map<expr, expr*>::find(expr*, expr*&) const ../src/util/obj_hashtable.h:162
    #6 0x1221d73 in smt::theory_lra::imp::should_research(ref_vector<expr, ast_manager>&) ../src/smt/theory_lra.cpp:3950
    #7 0x11ed5cd in smt::theory_lra::should_research(ref_vector<expr, ast_manager>&) ../src/smt/theory_lra.cpp:4123
    #8 0xfdd560 in smt::context::should_research(lbool) ../src/smt/smt_context.cpp:3257
    #9 0xfdfb68 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3493
    #10 0xd45fdc in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #11 0xd44c39 in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296
    #12 0x10fb478 in check_sat_core2 ../src/smt/smt_solver.cpp:190
    #13 0x1a1e63b in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #14 0x1a226a5 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #15 0x5e190a in solver::check_sat(ref_vector<expr, ast_manager> const&) ../src/solver/solver.h:149
    #16 0xb28547 in qe::qsat::check_sat() ../src/qe/qsat.cpp:646
    #17 0xb2d4e6 in qe::qsat::elim(ref_vector<app, ast_manager>&, expr*) ../src/qe/qsat.cpp:1100
    #18 0xb2c82b in qe::qsat::elim_rec(expr*) ../src/qe/qsat.cpp:1052
    #19 0xb2e858 in qe::qsat::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/peisen/test/tofuzz/z3-debug/build/z3+0xb2e858)
    #20 0x1a9e4a1 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:788
    #21 0x1a92cd0 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150

NSB comment: this was fixed

[rainoftime]

Assertion violation at ast/rewriter/rewriter.cpp:83 (proof)
z3 commit 48d4d8d

(set-logic UFLIA)
(set-option :proof true)
(assert (! (or (forall ((q2 Bool) (q3 Int) (q4 Bool) (q5 Int) (q6 Bool)) (<= q3 0)) (exists ((q2 Bool) (q3 Int) (q4 Bool) (q5 Int) (q6 Bool)) (> 580 q5))) :named IP_3))
(check-sat)

ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter.cpp
Line: 83
rewrites_from(k, pr)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

NSB comment: this was fixed

[rainoftime]

Assertion violation at qe/qe_arith.cpp:212
z3 commit 48d4d8d

(set-logic ALIA)
(set-option :model_validate true)
(set-option :rewriter.eq2ineq true)
(set-option :smt.arith.solver 2)
(declare-const arr-3301600726807452095_3301600726807452095-0 (Array (Array Int Int) (Array Int Int)))
(declare-const arr-525930757296696326_-1315234738400079307-0 (Array Bool (Array (Array Int Int) (Array Int Int))))
(declare-const arr-2119198754882234686_-2443551786470090660-0 (Array (Array Bool (Array (Array Int Int) (Array Int Int))) Int))
(assert (exists ((q71 (Array Int Bool)) (q72 (Array (Array (Array Bool (Array (Array Int Int) (Array Int Int))) Int) (Array (Array Bool (Array (Array Int Int) (Array Int Int))) Int))) (q73 (Array Int (Array (Array Int Int) (Array Int Int)))) (q74 Int) (q75 (Array Int Bool))) (= 0 q74)))
(push 1)
(assert (<= (mod (select arr-2119198754882234686_-2443551786470090660-0 (store arr-525930757296696326_-1315234738400079307-0 false arr-3301600726807452095_3301600726807452095-0)) 41) 0))
(check-sat)
(check-sat-using (then simplify qe2)

sat
ASSERTION VIOLATION
File: ../src/qe/qe_arith.cpp
Line: 212
Failed to verify: a.is_numeral(val, r)

NSB comment: this was fixed

[rainoftime]

At commit eaffe46

(set-option :smt.string_solver z3str3)
(declare-const i3 Int)
(declare-const Str10 String)
(declare-const Str12 String)
(assert (or (str.contains Str12 Str10) (>= i3 0)))
(check-sat-using (then simplify propagate-values qe2))

ASSERTION VIOLATION
 File: ../src/util/vector.h
 Line: 404
 !empty()
 (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

@mtrberzi - the last one is in theory_str.cpp.

It has:

    void theory_str::pop_scope_eh(unsigned num_scopes) {
        sLevel -= num_scopes;
        TRACE("str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;);
        candidate_model.reset();

        m_basicstr_axiom_todo.reset();
        m_concat_axiom_todo.reset();
        m_concat_eval_todo.reset();
        m_library_aware_axiom_todo.reset();

The m_libraray_aware_axiom_todo vector is "owned" by the trail stack. So the life-time of objects within that vector should follow the lifetime of the library_aware_axiom_trail_stack object according the the places where that vector gets updated:

                    m_library_aware_axiom_todo.push_back(n);
                    m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));

At this point m_library_aware_trail_stack is reset two other places in the code.

[nunoplopes]

@rainoftime I can't reproduce any of the new crashes you posted here. Can you please confirm if they repro for you with the latest version? Thanks!

[rainoftime]

The fixed tests were deleted

[rainoftime]

At commit b7caabb

(set-logic QF_NIA)
(declare-fun _substvar_448_ () Bool)
(declare-fun _substvar_453_ () Bool)
(declare-fun _substvar_594_ () Bool)
(declare-fun _substvar_627_ () Bool)
(declare-fun _substvar_629_ () Bool)
(declare-fun _substvar_679_ () Bool)
(declare-fun _substvar_683_ () Bool)
(declare-fun _substvar_686_ () Bool)
(declare-fun _substvar_781_ () Bool)
(declare-fun _substvar_798_ () Int)
(declare-fun _substvar_827_ () Bool)
(set-option :smt.arith.bounded_expansion true)
(set-option :rewriter.elim_and true)
(set-option :rewriter.cache_all true)
(declare-const v5 Bool)
(declare-const v8 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const i6 Int)
(declare-const i11 Int)
(declare-const i12 Int)
(push 1)
(declare-const v33 Bool)
(declare-const v34 Bool)
(assert _substvar_827_)
(assert (or v34 (not (= true v13 v8 true true)) (distinct 327 (- 0 23 i6 i11 (abs i6)) (* i11 (+ 14 _substvar_798_ i12 14 i11) 32))))
(assert (or _substvar_594_ v12 _substvar_686_))
(assert v33)
(assert _substvar_627_)
(assert _substvar_679_)
(assert _substvar_683_)
(assert _substvar_629_)
(assert v5)
(assert _substvar_781_)
(check-sat)
(assert _substvar_448_)
(assert _substvar_453_)
(check-sat-using (then simplify card2bv ctx-solver-simplify nnf dom-simplify qfnia))

sat
=================================================================
==57464==ERROR: AddressSanitizer: heap-use-after-free on address 0x60700005e6e4 at pc 0x000000468183 bp 0x7fff29cb99f0 sp 0x7fff29cb99e0
READ of size 4 at 0x60700005e6e4 thread T0
    #0 0x468182 in ast::hash() const ../src/ast/ast.h:501
    #1 0x5d4169 in obj_map<expr, expr*>::key_data::hash() const ../src/util/obj_hashtable.h:77
    #2 0x5d3541 in obj_map<expr, expr*>::obj_map_entry::get_hash() const ../src/util/obj_hashtable.h:86
    #3 0x5d1bf2 in core_hashtable<obj_map<expr, expr*>::obj_map_entry, obj_hash<obj_map<expr, expr*>::key_data>, default_eq<obj_map<expr, expr*>::key_data> >::insert(obj_map<expr, expr*>::key_data&&) ../s
rc/util/hashtable.h:403
    #4 0x5d0da0 in obj_map<expr, expr*>::insert(expr*, expr* const&) ../src/util/obj_hashtable.h:141
    #5 0x1221151 in smt::theory_lra::imp::add_theory_assumptions(ref_vector<expr, ast_manager>&) ../src/smt/theory_lra.cpp:3967
    #6 0x11ee7f7 in smt::theory_lra::add_theory_assumptions(ref_vector<expr, ast_manager>&) ../src/smt/theory_lra.cpp:4155
    #7 0xfe0b9c in smt::context::add_theory_assumptions(ref_vector<expr, ast_manager>&) ../src/smt/smt_context.cpp:3479
    #8 0xfe0f24 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3497
    #9 0xd4772c in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #10 0xd46389 in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296
    #11 0xc6b426 in ctx_solver_simplify_tactic::simplify_bool(expr*, obj_ref<expr, ast_manager>&) ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:282
    #12 0xc6a59c in ctx_solver_simplify_tactic::reduce(obj_ref<expr, ast_manager>&) ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:201
    #13 0xc68d75 in ctx_solver_simplify_tactic::reduce(goal&) ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:107
    #14 0xc68955 in ctx_solver_simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:82
    #15 0x1aa8d71 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:937
    #16 0x1aa1944 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:113
    #17 0x1aa1a93 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #18 0x1aa1a93 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #19 0x1aa771b in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:788
    #20 0x1a9bf4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #21 0x1a9c3e5 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::_
_cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:170
    #22 0x19b0a0a in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:222
    #23 0x1977a7b in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
    #24 0x197828c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
    #25 0x197964d in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #26 0x1958656 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #27 0x43c402 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:90
    #28 0x4545c2 in main ../src/shell/main.cpp:352

[rainoftime]

Another instance of ast.h:501

(set-logic QF_LIA)
(declare-fun _substvar_1416_ () Int)
(declare-fun _substvar_1541_ () Bool)
(set-option :smt.arith.bounded_expansion true)
(set-option :rewriter.push_ite_arith true)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i10 Int)
(declare-const v35 Bool)
(declare-const i14 Int)
(declare-const i15 Int)
(assert (or (xor (distinct (+ 0 _substvar_1416_ 343 917 i10) 819) _substvar_1541_ true true true true false true (= 0 (+ 247 (div (* i1 83 83) 463) 0 (abs i2) i3))) v35 v35))
(minimize (+ i3 0))
(minimize (+ i14 i15))
(check-sat)

[NikolajBjorner]

latest commit should take care of the last two reports

[rainoftime]

commit fa9cf0f

(set-logic AUFBV)
(declare-fun _substvar_36_ () (_ BitVec 10))
(set-option :rewriter.split_concat_eq true)
(set-option :smt.threads 3)
(assert (not (forall ((q7 Bool) (q8 Bool) (q9 (_ BitVec 21)) (q10 Bool) (q11 (_ BitVec 21))) (not (= q11 q9 q11 (concat #b01111000010 _substvar_36_))))))
(check-sat)
(check-sat-using (then simplify ctx-solver-simplify))


sat
=================================================================
sat
=================================================================
==126253==ERROR: AddressSanitizer: heap-use-after-free on address 0x6160001a5e90 at pc 0x000002666157 bp 0x7f9936880160 sp 0x7f9936880150
READ of size 8 at 0x6160001a5e90 thread T1
==126253==AddressSanitizer: while reporting a bug found another one. Ignoring.
    #0 0x2666156 in ptr_hash_entry<char const>::is_used() const ../src/util/hashtable.h:99
    #1 0x2665d53 in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::find_core(char const* const&) const ../src/util/hashtable.h:517
    #2 0x26650fa in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::contains(char const* const&) const ../src/util/hashtable.h:535
    #3 0x26abefe in is_trace_enabled(char const*) ../src/util/trace.cpp:55
    #4 0x27135c1 in mpz_manager<true>::machine_div(mpz const&, mpz const&, mpz&) ../src/util/mpz.cpp:569
    #5 0x2714255 in mpz_manager<true>::div(mpz const&, mpz const&, mpz&) ../src/util/mpz.cpp:628

[rainoftime]

At 1e6d2fb

sat
ASSERTION VIOLATION
File: ../src/nlsat/nlsat_interval_set.cpp
Line: 97
sign <= 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

(set-logic QF_AUFLIRA)
(declare-fun _substvar_777_ () Bool)
(declare-fun _substvar_793_ () Bool)
(declare-fun _substvar_936_ () Bool)
(declare-fun _substvar_845_ () Bool)
(declare-fun _substvar_848_ () Bool)
(set-option :rewriter.blast_distinct true)
(set-option :algebraic.factor false)
(set-option :nlsat.minimize_conflicts true)
(set-option :nlsat.shuffle_vars true)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r5 Real)
(push 1)
(declare-const v6 Bool)
(declare-const v16 Bool)
(assert (or v6 (<= 94.41153 (* (+ r5 r1 r0 69718878.0) 69718878.0 r5 r0)) _substvar_936_))
(assert _substvar_845_)
(assert _substvar_848_)
(assert (or v6 (distinct 69718878.0 (- r5 69718878.0 r0) 0.0)))
(assert _substvar_777_)
(assert (or v16 _substvar_793_ v6))
(check-sat)
(check-sat-using (then simplify add-bounds ctx-solver-simplify))

[rainoftime]

Soundness issue at 1e6d2fb

$z3 smt.string_solver=z3str3 xx.smt2
sat
$z3  xx.smt2
unsat
$ cat xx.smt2
(set-logic QF_S)
(declare-const Str4 String)
(assert (str.< Str4 Str4))
(check-sat)

[mtrberzi]

Z3str3 does not yet support str.< and str.<= but support for this feature is being worked on

[rainoftime]

At 1e6d2fb

(set-logic QF_SLIA)
(set-info :status sat)
(declare-fun x () (Seq Int))
(declare-fun y () (Seq Int))
(assert (not (= x y)))
(check-sat)

ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 170
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Performance regresssion from arith.solver=2 to arith.solver=6
Commit 2572440

(set-logic QF_NRA)
(declare-const r4 Real)
(declare-const r10 Real)
(push 1)
(assert (<= 992649700.0 r10 r10 (* r4 r4)))
(check-sat)

$ time z3 smt.arith.solver=2 xx.smt2                                                                                                                
sat

real    0m0.008s
user    0m0.004s
sys     0m0.000s
$ time z3 smt.arith.solver=6 timeout=60000 xx.smt2                                                                                                  
unknown

real    1m0.158s
user    1m0.112s
sys     0m0.048s

[rainoftime]

Performance regresssion from arith.solver=2 to arith.solver=6 (on QF_SLIA formula)
Commit 2572440

(set-logic QF_SLIA)
(declare-fun _substvar_140_ () Bool)
(declare-fun _substvar_141_ () Bool)
(declare-fun _substvar_147_ () Bool)
(declare-fun _substvar_152_ () Bool)
(declare-fun _substvar_154_ () Bool)
(declare-fun _substvar_259_ () Bool)
(declare-fun _substvar_299_ () Bool)
(declare-const v2 Bool)
(declare-const v7 Bool)
(declare-const v9 Bool)
(declare-const Str0 String)
(declare-const Str10 String)
(declare-const Str11 String)
(declare-const Str15 String)
(assert (>= (str.len Str15) 91))
(declare-const v12 Bool)
(push 1)
(assert _substvar_299_)
(assert (or v7 _substvar_141_ _substvar_140_))
(assert _substvar_147_)
(assert _substvar_152_)
(assert _substvar_154_)
(assert (or v12 v9 _substvar_259_))
(assert (or (str.contains Str0 (str.replace Str10 Str15 Str11)) v12 v2))
(check-sat)

$ time z3 smt.arith.solver=2 ss.smt2                                                                                                                                     
sat
real    0m1.851s
user    0m1.775s
sys     0m0.076s

$ time z3 smt.arith.solver=6 timeout=180000 ss.smt2                                                                                                                             
unknown
real    3m0.417s
user    3m27.108s
sys     1m29.128s

[rainoftime]

Performance issue on QF_S formula (z3str3)

(set-logic QF_S)
(declare-const Str1 String)
(declare-const Str4 String)
(assert (= false (=  true (xor true false (str.prefixof Str4 "") true false) true) false))
(assert (str.contains (str.++ "" "" (str.++ Str4 "caextk") Str1) (str.++ "" "yqibocfoiyfnrpbiblttxwzwlhnbefdtuvockczqioukonncjd" "uoezdalyseqzzlisdmgvoazgxlpufypjayotopfcrcdreqequn" Str4 "")))
(check-sat)

$time ./z3 smt.string_solver=seq xx.smt2
sat
real    0m0.484s
user    0m0.452s
sys     0m0.032s

$time ./z3 smt.string_solver=z3str3 timeout=600000  xx.smt2
unknown

real    10m0.117s
user    9m56.429s
sys     0m3.680s

[rainoftime]

Potential performance issue at 6cc52e0

(declare-const v1 Bool)
(declare-const v9 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const i10 Int)
(declare-const r1 Real)
(declare-const v19 Bool)
(declare-const i12 Int)
(assert (or (= 0 i6) v1))
(assert (< i12 0 798))
(assert (or (<= i10 23) (>= 8999883.0 0.1653 r1)))
(assert (or (= i10 0) (= (* (- i6 i6 i1 i0 23) i6) i6)))
(assert (or (= i10 i1) (=> (=> v9 (> i6 9 i1 53 i7)) v19)))
(assert (or (distinct (to_int (* (+ (- r1) 45106.0 (- 8999883.0) 8999883.0 (- 8999883.0)) 45106.0 (+ r1 8999883.0 45106.0 45106.0) (+ (- r1) 45106.0 (- 8999883.0) 8999883.0 (- 8999883.0)) 4.0)) 882) v9))
(check-sat)

$ time ./cvc4-2020-10-01-x86_64-linux-opt  -q f.smt2
sat
real    0m0.009s
user    0m0.009s
sys     0m0.000s
$ ./z3 smt.arith.solver=6 timeout=600000 xx.smt2
unknown

[rainoftime]

At 6cc52e0
z3 yields an invalid model for the LRA formula

(set-logic LRA)
(set-option :model_validate true)
(declare-const r9 Real)
(declare-const r14 Real)
(assert (exists ((q0 Bool) (q1 Bool) (q2 Bool)) (<= 0.4713721 r14 0.6023389)))
(push 1)
(assert (= 0.6023389 r9))
(check-sat)

When feeding the model to z3, it yields unsat.

(model 
  (define-fun r14 () Real
    0.0)
  (define-fun r9 () Real
    0.0)
)

---

Another formula

(set-logic QF_UFLIA)
(set-option :model_validate true)
(declare-const i4 Int)
(check-sat)
(assert true)
(check-sat)
(assert (= 4 i4))
(check-sat)

The model is trivially infeasible

sat
sat
sat
(error "line 8 column 10: an invalid model was generated")
(model 
  (define-fun i4 () Int
    0)
)

---

Fixed in 72b1e8a

[rainoftime]

At 1131fed, smt.arith.solver=6, 2 yield different results

(set-logic QF_LRA)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r4 Real)
(declare-const r10 Real)
(declare-const r11 Real)
(assert (or (< r10 (- 4.0 56488.5) r4 (+ 56488.5 r1)) (= 86585115806.0 r4 (+ 0.4677098 r10 41.0) r11)))
(maximize r0)
(check-sat)
(get-objectives)

z3 smt.arith.solver=6 xx.smt2
sat
(objectives
 (r0 (/ 1.0 2.0))
)
z3 smt.arith.solver=2 xx.smt2
sat
(objectives
 (r0 oo)
)

[rainoftime]

z3 commit ae7d767 throws an assertion failure on the following QF_ABV formula

ASSERTION VIOLATION
File: ../src/smt/theory_bv.cpp
Line: 1241
bit != ~bit2
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

(set-logic QF_ABV)
(declare-fun mem_35_57_4 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun R_EBX_6_67_3 () (_ BitVec 32))
(declare-fun R_EBP_0_60_2 () (_ BitVec 32))
(declare-fun R_ESP_1_58_1 () (_ BitVec 32))
(assert (let ((?v_0 (bvsub (bvsub R_ESP_1_58_1 (_ bv4 32)) (_ bv4 32)))) (let ((?v_6 (bvadd (bvadd ?v_0 (_ bv4 32)) (_ bv4 32))) (?v_2 (store (store (store (store mem_35_57_4 (bvadd ?v_0 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60_2 (_ bv24 32)))) (bvadd ?v_0 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60_2 (_ bv16 32)))) (bvadd ?v_0 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60_2 (_ bv8 32)))) (bvadd ?v_0 (_ bv0 32)) ((_ extract 7 0) R_EBP_0_60_2)))) (let ((?v_4 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_2 (_ bv134526656 32))) (bvshl (concat (_ bv0 24) (select ?v_2 (_ bv134526657 32))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_2 (_ bv134526658 32))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_2 (_ bv134526659 32))) (_ bv24 32)))) (?v_1 (bvsub (bvsub ?v_0 (_ bv4 32)) (_ bv4 32)))) (let ((?v_3 (store (store (store (store ?v_2 (bvadd ?v_1 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBX_6_67_3 (_ bv24 32)))) (bvadd ?v_1 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBX_6_67_3 (_ bv16 32)))) (bvadd ?v_1 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBX_6_67_3 (_ bv8 32)))) (bvadd ?v_1 (_ bv0 32)) ((_ extract 7 0) R_EBX_6_67_3)))) (let ((?v_7 (concat (_ bv0 24) (select ?v_3 ?v_4)))) (let ((?v_5 (store ?v_3 ?v_4 ((_ extract 7 0) (bvadd ?v_7 (_ bv1 32))))) (?v_8 (concat (_ bv0 24) ((_ extract 7 0) ?v_7)))) (let ((?v_9 (bvand (bvsub ?v_8 (_ bv56 32)) (_ bv255 32)))) (let ((?v_10 (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_8 (_ bv56 32)) (bvxor ?v_8 ?v_9)) (_ bv7 32)))) (_ bv1 1) (_ bv0 1)))) (= (_ bv1 1) (bvand (ite (not (= (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_57_4 (bvadd R_ESP_1_58_1 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_57_4 (bvadd R_ESP_1_58_1 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_57_4 (bvadd R_ESP_1_58_1 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_57_4 (bvadd R_ESP_1_58_1 (_ bv3 32)))) (_ bv24 32))) (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_5 (bvadd ?v_6 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd ?v_6 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd ?v_6 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_5 (bvadd ?v_6 (_ bv3 32)))) (_ bv24 32))))) (_ bv1 1) (_ bv0 1)) (bvand ((_ extract 0 0) (concat (_ bv0 31) (bvor (bvxor (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr ?v_9 (_ bv7 32)))) (_ bv1 1) (_ bv0 1)) ?v_10) (ite (= ?v_9 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (bvand (bvnot ?v_10) (_ bv1 1))))))))))))))
(check-sat)

[rainoftime]

z3 commit ae7d767 soundness issue (the model validator cannot decide that the model is invalid)

z3  yy.smt2 model_validate=true
sat
z3  yy.smt2
sat
cvc4 -q yy.smt2
unsat

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun u () Real)
(assert (not (exists ((s Real)) (=> (and (= i 0.0 (+ q (/ a a)) 0.0 0.0) (<= a (- 2.0 d (- u)))) (= (<= s 0.0) (<= 0.0 i (* d (- u))))))))
(assert (exists ((t Real)) (and (<= (* (/ 2.0 0.0 0.0) j) k) (= (- b e) 1.0))))
(assert (= b (+ e p) 0.0 (+ u p) 0.0 (/ i 0.0)))
(check-sat)

[zhendongsu]

For the above case, see #2650 (and check with nlsat.check_lemmas=true).

[rainoftime]

At ae7d767 invalid model issue.
After changing LRA toQF_LRA, z3 can work correctly

$ cat xx.smt2
(set-logic LRA)
(declare-const r0 Real)
(declare-const r1 Real)
(push 1)
(check-sat)
(assert (= r1 0.74 r0))
(check-sat)

$z3 xx.smt2 model_validate=true
sat
sat
(error "line 7 column 10: an invalid model was generated")
(model 
  (define-fun r0 () Real
    0.0)
  (define-fun r1 () Real
    0.0)
)

---

Another instance

$ cat xx.smt2
(set-option :model_validate true)
(declare-const r8 Real)
(declare-const i12 Int)
(assert (is_int r8))
(push 1)
(assert (= 52 i12))
(check-sat)

$ z3 xx.smt2
sat
(error "line 7 column 10: an invalid model was generated")
(model 
  (define-fun r8 () Real
    0.0)
  (define-fun i12 () Int
    0)
)

Fixed in 72b1e8a

[rainoftime]

At commit 72b1e8a

$ ./z3 xx.smt2 smt.arith.solver=6
ASSERTION VIOLATION
File: ../src/math/lp/int_solver.cpp
Line: 415
lrac.m_r_solver.calc_current_x_is_feasible_include_non_basis() == lrac.m_r_solver.current_x_is_feasible()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
$ cat xx.smt2
(declare-const i1 Int)
(declare-fun ufrb3 (Real Real Real) Bool)
(assert (not (>= i1 (mod i1 30))))
(push 1)
(assert (ufrb3 88.0 5616379.0 0.0))
(check-sat)

[rainoftime]

At 2841796, z3 gives an invalid model

(set-logic QF_AUFNIA)
(declare-const i1 Int)
(declare-const i0 Int)
(declare-const i4 Int)
(declare-const i7 Int)
(assert (< 0 4 i0 i7 i4))
(push 1)
(assert (distinct i1 4))
(check-sat)

./z3 model_validate=true xx.smt2
sat
(error "line 9 column 10: an invalid model was generated")
(model 
  (define-fun i4 () Int
    0)
  (define-fun i7 () Int
    0)
  (define-fun i1 () Int
    5)
  (define-fun i0 () Int
    0)
)