[Consolidated] soundness issues, invalid models, and crashes for options "tactic.default_tactic=smt sat.euf=true" (2)

[zhendongsu]

Commit: ba56bfa
OS: Ubuntu 18.04

Refutation unsoundness:

[526] % z3release small.smt2
sat
[527] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[528] % cat small.smt2
(declare-const a Real)
(assert (not (< (* a a) 0 0)))
(check-sat)
[529] % 

[zhendongsu]

[516] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_internalize.cpp
Line: 278
Failed to verify: v != sat::null_bool_var

Z3 4.8.11.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[517] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/q_mam.cpp
Line: 3777
t->has_candidates()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[518] % 
[518] % cat small.smt2
(declare-datatypes ((a 0)) (((b (c a) (k a)) (d (l a)) (m (e a) (f a)) (g))))
(declare-fun h () a)
(declare-fun i (a) a)
(assert
 (forall ((j a))
  (= (m j j)
   (ite (and ((_ is b) j))
    (m (i (d (c (l j)))) (i (d (k j))))
    (ite (and ((_ is m) j))
     (b (i (d (e (l j)))) (i (d (f (l j)))))
     (ite (and ((_ is d) j))
      (i (l (l j))) h))))))
(check-sat)
[519] % 

[zhendongsu]

Solution unsoundness:

[507] % z3release small.smt2
unsat
[508] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
[509] % cat small.smt2
(declare-fun a () Real)
(assert (forall ((b Real)) (and (= a b) (= 0 0))))
(check-sat)
[510] % 

[zhendongsu]

[528] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[529] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_model.cpp
Line: 214
Failed to verify: arg

[530] % z3san tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==20408==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x55bbd7e5036e bp 0x7ffc5fa43fd0 sp 0x7ffc5fa43ef0 T0)
==20408==The signal is caused by a READ memory access.
==20408==Hint: address points to the zero page.
    #0 0x55bbd7e5036d in ast::get_kind() const ../src/ast/ast.h:501
    #1 0x55bbd7e5036d in is_app(ast const*) ../src/ast/ast.h:914
    #2 0x55bbd7e5036d in ast_manager::are_equal(expr*, expr*) const ../src/ast/ast.cpp:1643
    #3 0x55bbd6b7bb62 in func_entry::eq_args(ast_manager&, unsigned int, expr* const*) const ../src/model/func_interp.cpp:57
    #4 0x55bbd6b7bb62 in func_interp::get_entry(expr* const*) const ../src/model/func_interp.cpp:180
    #5 0x55bbd5c090db in euf::solver::values2model(top_sort<euf::enode> const&, ref<model>&) ../src/sat/smt/euf_model.cpp:216
    #6 0x55bbd5c10edb in euf::solver::update_model(ref<model>&) ../src/sat/smt/euf_model.cpp:73
    #7 0x55bbd5b88e67 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:109
    #8 0x55bbd5b8b105 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:202
    #9 0x55bbd6a9c4f8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:924
    #10 0x55bbd6a670de in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #11 0x55bbd6a68a87 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
    #12 0x55bbd68b22f0 in check_sat_core2 ../src/solver/tactic2solver.cpp:187
    #13 0x55bbd68d58ef in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #14 0x55bbd68ee334 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #15 0x55bbd68c32a6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:332
    #16 0x55bbd683d8c5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1647
    #17 0x55bbd679ad93 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2607
    #18 0x55bbd679ad93 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2949
    #19 0x55bbd679ad93 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3141
    #20 0x55bbd674ff75 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3190
    #21 0x55bbd3ab04ff in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #22 0x55bbd3a5ae24 in main ../src/shell/main.cpp:371
    #23 0x7f842b2a4b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #24 0x55bbd3a70c79 in _start (/local/suz-local/software/z3san/build-05312021190355-ba56bfa/z3+0x208c79)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:501 in ast::get_kind() const
==20408==ABORTING
[531] % 
[531] % cat small.smt2
(set-option :smt.arith.reflect false)
(declare-const x Real)
(assert (= 0 (* (/ 0 0) (/ 0 (- 1.0) (* x x)))))
(check-sat)
[532] % 

[zhendongsu]

Invalid model:

[518] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(
  (define-fun a () Real
    0.0)
  (define-fun b () Bool
    false)
  (define-fun c () Bool
    false)
)
[519] % cat small.smt2
(declare-const a Real)
(declare-const b Bool)
(declare-const c Bool)
(assert (or b c))
(maximize a)
(check-sat)
(get-model)
[520] % 

[rainoftime]

Refutation soundness

(declare-const x Bool)
(assert (exists ((s Real)) (or x (not x))))
(check-sat)

 z3 xx.smt2
sat
z3 tactic.default_tactic=smt sat.euf=true xx.smt2
unsat

[rainoftime]

Invalid model

(declare-fun y () Int)
(declare-fun x () Int)
(assert (and (= 1 y) (< 1 x)))
(check-sat-using (then dom-simplify add-bounds normalize-bounds smt))

z3 tactic.default_tactic=smt sat.euf=true model_validate=true delta.out.smt2
sat
(error "line 4 column 68: an invalid model was generated")

[rainoftime]

src/ast/ast.h:934

(assert (exists ((T2_673 (_ BitVec 1))) (forall ((T1_734 (_ BitVec 1))) (let (($x31 true))))))
(check-sat)


z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 934
is_quantifier(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

heap-use-after-free

(declare-fun A (Int) Bool)
(declare-fun B (Int) Bool)
(declare-fun C (Int) Bool)
(declare-fun D (Int) Bool)
(assert (forall ((x Int)) (=> (or (A x) (B x)) (D x))))
(assert (forall ((x Int)) (iff (D x) (C x))))
(assert (B 1))
(check-sat)

READ of size 8 at 0x603000018b38 thread T0
    #0 0x247d2f8 in q::mam_impl::propagate() /home/z3-debug/build/../src/sat/smt/q_mam.cpp:3776:31
    #1 0x23ef98d in q::ematch::propagate(bool) /home/z3-debug/build/../src/sat/smt/q_ematch.cpp:468:16
    #2 0x234f280 in q::solver::unit_propagate() /home//z3-debug/build/../src/sat/smt/q_solver.cpp:95:57
    #3 0x22521f5 in euf::solver::unit_propagate() /home//z3-debug/build/../src/sat/smt/euf_solver.cpp:336:24

[rainoftime]

src/sat/smt/arith_solver.cpp:833

(declare-fun rr1 () Real)
(assert (let (($x437 (and (= 0.0 (- rr1 rr1)) (not (= rr1 0.0)))))))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 833
is_registered_var(v)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/q_mam.cpp:2257

(declare-fun q (Int) Bool)
(assert (forall ((x Int)) (forall ((z Int)) (or (q z) (= z 1)))))
(check-sat)
(check-sat-using qffd)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
sat
ASSERTION VIOLATION
File: ../src/sat/smt/q_mam.cpp
Line: 2257
ctx.is_relevant(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/util/vector.h:474

(assert (forall ((z2 (_ BitVec 1))) (exists ((x (_ BitVec 2))) (= x (_ bv1 2)))))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 474
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/arith_solver.cpp:584

(set-option :rewriter.mul_to_power true)
(declare-fun x2 () Int)
(assert (and (< x2 1) (< x2 (- 1))))
(check-sat)

ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 584
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/array_solver.cpp:194

(declare-fun f () (Set Int))
(assert (= f (complement f)))
(check-sat-using bv)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/array_solver.cpp
Line: 194
can_beta_reduce(lambda)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/util/sat_literal.h:48

(declare-fun q (Int) Bool)
(declare-fun bb8 () Bool)
(declare-fun l3 () Bool)
(assert (let (($x6 (q 0)))))
(assert (= l3 (forall ((x1 Int)) (not (q x1)))))
(assert (= l3 (and bb8)))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true xx.smt2
ASSERTION VIOLATION
File: ../src/util/sat_literal.h
Line: 48
var() == v
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[zhendongsu]

Adding a few more tests:

[578] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/math/simplex/model_based_opt.cpp
Line: 185
index == 0 || r.m_type != t_mod || (mod(r.m_value, r.m_mod).is_zero())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[579] % cat small.smt2
(set-option :smt.ematching false)
(declare-sort a)
(declare-fun b (Int) a)
(assert (forall ((c Int)) (not (= (b (* 3 c)) (b 1)))))
(check-sat)
[580] %