search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.38k stars 1.48k forks source link

[consolidated] issues in the new core #6319

Closed zhendongsu closed 2 years ago

zhendongsu commented 2 years ago 
[533] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 470 15677: (<= (+ (* 2 #11884) (* -1 #11554)) 0) true
(sat
...
[534] % 
[534] % cat small.smt2 
(declare-fun p (Int) Int)
(assert (= (p 0) 1))
(assert (forall ((i Int)) (or (<= i 0) (= (p i) (* 2 (p (- i 1)))))))
(check-sat)
zhendongsu commented 2 years ago

Another similar instance:

[507] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 481 5766: (<= (+ (* 2 #12541) (* -1 #10498)) 0) true
(sat
...
[508] % 
[508] % cat small.smt2
(declare-fun o (Int) Int)
(define-fun p () Bool (and (forall ((i Int)) (= 0 (o 1)))))
(assert (and (= 1 (o 0)) (forall ((i Int)) (or (not (> i 0)) (= (o i) (* 2 (o (- i 1))))))))
(check-sat)
zhendongsu commented 2 years ago 
[507] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 1344 6624: (<= (array-ext[0] (if #4039 #3562 #4281) (store #4033 2 #3570)) 2) false
(sat
...
[508] % cat small.smt2 
(declare-fun t ((Array Int (Array Int Real))) (Array Int (Array Int Real)))
(declare-fun p ((Array Int (Array Int Real)) (Array Int (Array Int Real))) (Array Int (Array Int Real)))
(assert (forall ((a (Array Int (Array Int Real))) (b (Array Int (Array Int Real)))) (distinct (select (p b (p b (t b))) 1) (select (p a (p b (p (t b) (t b)))) 0))))
(check-sat)
zhendongsu commented 2 years ago 
[513] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 56 260: (= (select (store #378 8855 #129) A!38) (select (const #251) A!38)) false
(sat
...
[514] % cat small.smt2 
(declare-fun h () (Array Int (Array Int Real)))
(declare-fun d (Int Int) Int)
(declare-fun t (Int Int Real) (Array Int (Array Int Real)))
(assert (forall ((A Int) (L Int) (U Int) (J Int) (B Int) (V Real)) (= V (select (select (t (d L U) (d U B) 0.0) A) J))))
(assert (not (=> true (forall ((A Real)) (forall ((A Real)) (and (forall ((A Int)) (> A 0)) (forall ((A Int) (M Int)) (or (= 0.0 (select (select h A) 0)) (distinct M 0)))))))))
(check-sat)
zhendongsu commented 2 years ago 
[528] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 893 4091: (= (mod 1 (b!0 -17)) (mod0 1 (b!0 -17))) false
(sat
...
[529] % cat small.smt2 
(set-option :smt.arith.ignore_int true)
(assert (forall ((a Int)) (exists ((b Int)) (and (<= 0 (+ a b)) (<= 0 (mod 1 b))))))
(check-sat-using (then purify-arith smt))
zhendongsu commented 2 years ago 
[535] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 263 272: (bvule (extract[51:0] (bv_wrap x)) (extract[51:0] (bv_wrap y))) true
(sat
...
[536] % cat small.smt2 
(define-sort FPN () Float64)
(declare-fun x () FPN)
(declare-fun y () FPN)
(declare-fun r () FPN)
(assert (distinct r (fp.min x y)))
(check-sat-using qfufbv)
zhendongsu commented 2 years ago 
[542] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 33 173: (<= (* (to_int v!1) (div 2 #66)) 0) false
(sat
...
[543] % cat small.smt2 
(assert (forall ((v Real)) (exists ((x Real)) (forall ((y Real)) (or (< 0 (+ x v)) (<= 0 (mod (+ 1 (mod 2 (to_int v))) (to_int y))))))))
(check-sat-using ufbv)
zhendongsu commented 2 years ago

Refutation unsoundness:

[535] % z3release model_validate=true small.smt2 
sat
[536] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
unsat
[537] % cat small.smt2 
(assert (bvuge (_ bv0 32) (bvand (_ bv0 32) (bvmul (bvxnor (_ bv0 32) (_ bv0 32)) ((_ zero_extend 24) (_ bv30 8))))))
(check-sat)
zhendongsu commented 2 years ago

A likely related instance:

[571] % z3release model_validate=true small.smt2 
sat
[572] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
unsat
[573] % cat small.smt2 
(declare-fun m () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (= (_ bv1 1) (ite (distinct (_ bv0 32) ((_ zero_extend 24) (select m (bvmul (bvnand ((_ zero_extend 24) (select m (_ bv0 32))) (bvlshr ((_ zero_extend 24) (select m (_ bv0 32))) ((_ zero_extend 24) (select m (_ bv0 32))))) (bvshl (_ bv1 32) ((_ zero_extend 24) (select m (_ bv0 32)))))))) (_ bv1 1) (_ bv0 1))))
(check-sat)
zhendongsu commented 2 years ago 
[561] % z3release small.smt2
sat
[562] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
num-conflicts: 1
ASSERTION VIOLATION
File: ../src/sat/sat_solver.cpp
Line: 2557
Failed to verify: idx > 0

Z3 4.11.2.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[563] % cat small.smt2
(declare-datatypes ((a 0)) (((b (c Int) (d a)) (g))))
(define-fun-rec e ((f a)) Int (ite ((_ is b) f) (- 1 (e (d f))) 0))
(assert (distinct (e (b 0 g)) 0))
(check-sat)
merlinsun commented 2 years ago 
$ z3 model_validate=true tactic.default_tactic=smt sat.euf=true small.smt2
failed to verify: (not (= ar!72 ((_ map (or (Bool Bool) Bool)) r!73 ar!72)))
evaluated to false
(params drat.disable true keep_cardinality_constraints true pb.solver solver)
......
$ cat small.smt2
(declare-fun b ((Array Int (Array Int Real)) Int) Bool)
(declare-fun v () Int)
(declare-fun a () Int)
(declare-fun r () (Array Int (Array Int Real)))
(assert (or true (distinct (select (select r v) 0) (select (select r 0) a))))
(assert (forall ((r4 Int) (ar (Array Int Bool)) (r (Array Int Bool)) (va (Array Int (Array Int Real)))) (or (b va 0) (and (= 1 r4) (= ar ((_ map or) r ar))))))
(check-sat-using sat)
wintered commented 2 years ago

16ef89905d8b5702347021271bdd071d5bf80277

$z3release model_validate=true tactic.default_tactic=smt sat.euf=true bug.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(objectives
 (x oo)
)
$cat bug.smt2 
(declare-const x Int)
(declare-const y Int)
(assert (<= 1 y))
(assert (<= 1 (+ (- (+ 1 1) 0) 1)))
(maximize x)
(check-sat)
(get-objectives)
zhendongsu commented 2 years ago 
[531] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
sat
[532] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
sat
[533] % z3san tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
=================================================================
==25926==ERROR: AddressSanitizer: heap-use-after-free on address 0x603000009bc0 at pc 0x5570a1cad209 bp 0x7ffdf55fe380 sp 0x7ffdf55fe370
READ of size 8 at 0x603000009bc0 thread T0
    #0 0x5570a1cad208 in euf::solver::check() ../src/sat/smt/euf_solver.cpp:491
    #1 0x5570a3bc768c in sat::solver::final_check() ../src/sat/sat_solver.cpp:1773
    #2 0x5570a3bea5f0 in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1748
    #3 0x5570a3beae11 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1735
    #4 0x5570a3bebe4f in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1344
    #5 0x5570a1c99c59 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:73
    #6 0x5570a1c9ddbb in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:219
    #7 0x5570a2c7cedc in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1027
    #8 0x5570a2c4ab6e in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:153
    #9 0x5570a2c4c507 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:173
    #10 0x5570a2abb1f8 in check_sat_core2 ../src/solver/tactic2solver.cpp:229
    #11 0x5570a2adec7f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #12 0x5570a2af7ee4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #13 0x5570a2acc406 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #14 0x5570a2a43cc5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1693
    #15 0x5570a299d2c3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611
    #16 0x5570a299d2c3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953
    #17 0x5570a299d2c3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3162
    #18 0x5570a29525a5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3211
    #19 0x55709fa2ad01 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:144
    #20 0x55709f9fefb1 in main ../src/shell/main.cpp:381
    #21 0x7f25640b7c86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
    #22 0x55709fa0bbd9 in _start (/local/suz-local/software/z3san/build-09152022074100-0888988/z3+0x1fbbd9)

0x603000009bc0 is located 16 bytes inside of 24-byte region [0x603000009bb0,0x603000009bc8)
freed by thread T0 here:
    #0 0x7f25650c3f30 in realloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdef30)
    #1 0x5570a4689a01 in memory::reallocate(void*, unsigned long) ../src/util/memory_manager.cpp:323
    #2 0x5570a1cc83b4 in vector<euf::th_solver*, false, unsigned int>::expand_vector() ../src/util/vector.h:202
    #3 0x5570a1cc83b4 in vector<euf::th_solver*, false, unsigned int>::push_back(euf::th_solver* const&) ../src/util/vector.h:523
    #4 0x5570a1cc83b4 in scoped_ptr_vector<euf::th_solver>::push_back(euf::th_solver*) ../src/util/scoped_ptr_vector.h:46
    #5 0x5570a1cc83b4 in euf::solver::add_solver(euf::th_solver*) ../src/sat/smt/euf_solver.cpp:153
    #6 0x5570a1ccaf5d in euf::solver::get_solver(int, func_decl*) ../src/sat/smt/euf_solver.cpp:141
    #7 0x5570a1cd047f in euf::solver::func_decl2solver(func_decl*) ../src/sat/smt/euf_solver.h:146
    #8 0x5570a1cd047f in euf::solver::expr2solver(expr*) ../src/sat/smt/euf_solver.cpp:91
    #9 0x5570a1ceda9e in euf::solver::internalize(expr*, bool) ../src/sat/smt/euf_internalize.cpp:42
    #10 0x5570a1ceda9e in euf::solver::e_internalize(expr*) ../src/sat/smt/euf_internalize.cpp:456
    #11 0x5570a208c67d in array::solver::assert_select_as_array_axiom(app*, app*) ../src/sat/smt/array_axioms.cpp:386
    #12 0x5570a2098301 in array::solver::assert_select(unsigned int, array::solver::axiom_record&) ../src/sat/smt/array_axioms.cpp:119
    #13 0x5570a209e0eb in array::solver::assert_axiom(unsigned int) ../src/sat/smt/array_axioms.cpp:64
    #14 0x5570a209e0eb in array::solver::propagate_axiom(unsigned int) ../src/sat/smt/array_axioms.cpp:50
    #15 0x5570a2037c64 in array::solver::unit_propagate() ../src/sat/smt/array_solver.cpp:148
    #16 0x5570a209d7bb in array::solver::add_delayed_axioms() ../src/sat/smt/array_axioms.cpp:623
    #17 0x5570a2030c97 in array::solver::check() ../src/sat/smt/array_solver.cpp:99
    #18 0x5570a1cacddb in operator() ../src/sat/smt/euf_solver.cpp:483
    #19 0x5570a1cacddb in euf::solver::check() ../src/sat/smt/euf_solver.cpp:496
    #20 0x5570a3bc768c in sat::solver::final_check() ../src/sat/sat_solver.cpp:1773
    #21 0x5570a3bea5f0 in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1748
    #22 0x5570a3beae11 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1735
    #23 0x5570a3bebe4f in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1344
    #24 0x5570a1c99c59 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:73
    #25 0x5570a1c9ddbb in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:219
    #26 0x5570a2c7cedc in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1027
    #27 0x5570a2c4ab6e in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:153
    #28 0x5570a2c4c507 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:173
    #29 0x5570a2abb1f8 in check_sat_core2 ../src/solver/tactic2solver.cpp:229
    #30 0x5570a2adec7f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #31 0x5570a2af7ee4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #32 0x5570a2acc406 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #33 0x5570a2a43cc5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1693
    #34 0x5570a299d2c3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611
    #35 0x5570a299d2c3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953
    #36 0x5570a299d2c3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3162
    #37 0x5570a29525a5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3211
    #38 0x55709fa2ad01 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:144

previously allocated by thread T0 here:
    #0 0x7f25650c3b40 in __interceptor_malloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeb40)
    #1 0x5570a468993d in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:290
    #2 0x5570a1cc9529 in vector<euf::th_solver*, false, unsigned int>::expand_vector() ../src/util/vector.h:183
    #3 0x5570a1cc9529 in vector<euf::th_solver*, false, unsigned int>::push_back(euf::th_solver* const&) ../src/util/vector.h:523
    #4 0x5570a1cc9529 in scoped_ptr_vector<euf::th_solver>::push_back(euf::th_solver*) ../src/util/scoped_ptr_vector.h:46
    #5 0x5570a1cc9529 in euf::solver::add_solver(euf::th_solver*) ../src/sat/smt/euf_solver.cpp:153
    #6 0x5570a1ccaf5d in euf::solver::get_solver(int, func_decl*) ../src/sat/smt/euf_solver.cpp:141
    #7 0x5570a1cd047f in euf::solver::func_decl2solver(func_decl*) ../src/sat/smt/euf_solver.h:146
    #8 0x5570a1cd047f in euf::solver::expr2solver(expr*) ../src/sat/smt/euf_solver.cpp:91
    #9 0x5570a1cf6319 in euf::solver::visit(expr*) ../src/sat/smt/euf_internalize.cpp:105
    #10 0x5570a1fa9ca9 in euf::th_internalizer::visit_rec(ast_manager&, expr*, bool, bool, bool) ../src/sat/smt/sat_th.cpp:45
    #11 0x5570a1cecf76 in euf::solver::internalize(expr*, bool, bool, bool) ../src/sat/smt/euf_internalize.cpp:77
    #12 0x5570a1c81997 in goal2sat::imp::convert_euf(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:659
    #13 0x5570a1c8617d in goal2sat::imp::convert_atom(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:274
    #14 0x5570a1c873f0 in goal2sat::imp::visit(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:370
    #15 0x5570a1c881fe in goal2sat::imp::process(expr*, bool, bool) ../src/sat/tactic/goal2sat.cpp:759
    #16 0x5570a1c957d3 in goal2sat::imp::process(expr*) ../src/sat/tactic/goal2sat.cpp:860
    #17 0x5570a1c957d3 in goal2sat::imp::operator()(goal const&) ../src/sat/tactic/goal2sat.cpp:949
    #18 0x5570a1c9924b in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:53
    #19 0x5570a1c9ddbb in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:219
    #20 0x5570a2c7cedc in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1027
    #21 0x5570a2c4ab6e in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:153
    #22 0x5570a2c4c507 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:173
    #23 0x5570a2abb1f8 in check_sat_core2 ../src/solver/tactic2solver.cpp:229
    #24 0x5570a2adec7f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #25 0x5570a2af7ee4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #26 0x5570a2acc406 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #27 0x5570a2a43cc5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1693
    #28 0x5570a299d2c3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611
    #29 0x5570a299d2c3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953
    #30 0x5570a299d2c3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3162
    #31 0x5570a29525a5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3211
    #32 0x55709fa2ad01 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:144
    #33 0x55709f9fefb1 in main ../src/shell/main.cpp:381
    #34 0x7f25640b7c86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)

SUMMARY: AddressSanitizer: heap-use-after-free ../src/sat/smt/euf_solver.cpp:491 in euf::solver::check()
Shadow bytes around the buggy address:
  0x0c067fff9320: fa fa fd fd fd fa fa fa fd fd fd fa fa fa fd fd
  0x0c067fff9330: fd fd fa fa fd fd fd fa fa fa fd fd fd fa fa fa
  0x0c067fff9340: fd fd fd fa fa fa fd fd fd fa fa fa fd fd fd fa
  0x0c067fff9350: fa fa fd fd fd fa fa fa fd fd fd fa fa fa 00 00
  0x0c067fff9360: 06 fa fa fa 00 00 00 fa fa fa 00 00 00 fa fa fa
=>0x0c067fff9370: 00 00 00 fa fa fa fd fd[fd]fa fa fa fd fd fd fa
  0x0c067fff9380: fa fa fd fd fd fd fa fa 00 00 04 fa fa fa fd fd
  0x0c067fff9390: fd fa fa fa fd fd fd fa fa fa fd fd fd fa fa fa
  0x0c067fff93a0: fd fd fd fd fa fa fd fd fd fa fa fa fd fd fd fa
  0x0c067fff93b0: fa fa 00 00 00 00 fa fa fd fd fd fa fa fa fd fd
  0x0c067fff93c0: fd fd fa fa 00 00 00 fa fa fa 00 00 00 00 fa fa
Shadow byte legend (one shadow byte represents 8 application bytes):
  Addressable:           00
  Partially addressable: 01 02 03 04 05 06 07 
  Heap left redzone:       fa
  Freed heap region:       fd
  Stack left redzone:      f1
  Stack mid redzone:       f2
  Stack right redzone:     f3
  Stack after return:      f5
  Stack use after scope:   f8
  Global redzone:          f9
  Global init order:       f6
  Poisoned by user:        f7
  Container overflow:      fc
  Array cookie:            ac
  Intra object redzone:    bb
  ASan internal:           fe
  Left alloca redzone:     ca
  Right alloca redzone:    cb
==25926==ABORTING
[534] % cat small.smt2 
(define-fun f ((x Int)) Int x)
(declare-fun h (Int) Int)
(assert (= f h))
(assert (= 0 (h 0)))
(check-sat)
zhendongsu commented 2 years ago 
[528] % z3release model_validate=true small.smt2 
sat
[529] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
sat
(error "line 5 column 21: an invalid model was generated")
[530] % cat small.smt2 
(declare-fun f (Int) Bool)
(declare-fun g (Int) Bool)
(assert (or (g 0) (= f g)))
(assert (forall ((x Int)) (f x)))
(check-sat-using ufbv)
zhendongsu commented 2 years ago 
[516] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 33 column 46: an invalid model was generated")
[517] % cat small.smt2
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun aa () Bool)
(declare-fun e () Bool)
(declare-fun f () Bool)
(declare-fun ab () Bool)
(declare-fun g () Bool)
(declare-fun h () Bool)
(declare-fun i () Bool)
(declare-fun j () Bool)
(declare-fun k () Bool)
(declare-fun l () Bool)
(declare-fun m () Bool)
(declare-fun n () Bool)
(declare-fun o () Bool)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(declare-fun t () Bool)
(declare-fun u () Bool)
(declare-fun v () Bool)
(declare-fun w () Bool)
(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-fun z () Bool)
(declare-fun ac () Bool)
(declare-fun ad () Bool)
(declare-fun ae () Bool)
(assert (distinct false true ae ad ac z y x w v u t s r q p o n m l k j i h g ab f e aa d c b a))
(check-sat-using (then sat-preprocess default))
zhendongsu commented 2 years ago

16ef899

$z3release model_validate=true tactic.default_tactic=smt sat.euf=true bug.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(objectives
 (x oo)
)
$cat bug.smt2 
(declare-const x Int)
(declare-const y Int)
(assert (<= 1 y))
(assert (<= 1 (+ (- (+ 1 1) 0) 1)))
(maximize x)
(check-sat)
(get-objectives)

Dominik: see Nikolaj's comment from https://github.com/Z3Prover/z3/issues/6116#issuecomment-1171870871 @wintered

merlinsun commented 2 years ago

https://github.com/Z3Prover/z3/commit/9118a93e44a0c33d2a7c427d1ad15c7ecf99f6e8 soundness issue

$ z3 small.smt2
sat
$ z3 tactic.default_tactic=smt sat.euf=true small.smt2
unsat
$ cat small.smt2
(assert (distinct (_ bv1 1) (_ bv0 1)))
(check-sat)
merlinsun commented 2 years ago

A related instance about https://github.com/Z3Prover/z3/issues/6319#issuecomment-1251771105

$ cat delta.smt2
(assert (distinct false true))
(check-sat)
$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
unsat
merlinsun commented 2 years ago

This instance is a little strange after reducing.

$ cat small.smt2 
(assert (distinct ((_ to_fp 8 24) roundNearestTiesToEven (/ 1 5))))
(check-sat-using (then sat-preprocess propagate-values))
(check-sat)
$ z3 small.smt2
unknown
sat
$ z3 small.smt2 tactic.default_tactic=smt sat.euf=true
unsat
unknown
zhendongsu commented 2 years ago 
[516] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 13 149: (= (* i w) 0) true
(sat
...
[517] % cat small.smt2
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const aa Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(declare-const h Int)
(declare-const i Int)
(declare-const j Int)
(declare-const k Int)
(declare-const l Int)
(declare-const m Int)
(declare-const n Int)
(declare-const o Int)
(declare-const p Int)
(declare-fun q () Int)
(declare-fun r () Int)
(declare-fun s () Int)
(declare-fun t () Int)
(declare-fun u () Int)
(declare-fun v () Int)
(declare-fun w () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(declare-fun ab () Int)
(declare-fun ac () Int)
(declare-fun ad () Int)
(declare-fun ae () Int)
(declare-fun af () Int)
(declare-fun ag () Int)
(assert (< c (+ t i u d o ag  h  l m w k v (* f e) (* ac s) (* j p))))
(assert (= r 0))
(assert (<= 0 (+ g b (* y n))))
(assert (< (+ m 1) 0 q (+ ab aa af z ae a)))
(assert (> (+ b ad t k c f x b w (* t ad)) 0))
(assert (< (+ b c (* i w)) h))
(assert (<= t 0))
(assert (< (+ b b i 1 m) 1))
(check-sat)
zhendongsu commented 2 years ago 
[511] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 1074 4748: (= (and (not #13445) (<= 24290 b!325)) (and (not #24583) (<= -7 b!325) (not #4898) (<= 642 #17287))) true
(sat
...
[512] % cat small.smt2
(set-option :sat.gc.burst true)
(declare-fun d (Int Int) Int)
(declare-fun e (Int Int) Int)
(declare-fun f () Int)
(declare-fun g () Int)
(assert (forall ((a Int) (b Int)) (= (d g b) (d b (d a 0)))))
(assert (forall ((c Int)) (= c (e f (d g c)))))
(check-sat)
NikolajBjorner commented 2 years ago

moving to #6364

NikolajBjorner commented 2 years ago

moved open issues to #6364 optimization issue was fixed now. The new core should be disabled for arithmetical optimization but enabled for core-based maxsat instances.