Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[consolidated] issues in the new core #6319

Closed
zhendongsu opened this issue Sep 3, 2022 · 22 comments
Closed

[consolidated] issues in the new core #6319

zhendongsu opened this issue Sep 3, 2022 · 22 comments

Comments

@zhendongsu
Copy link 

[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
Copy link
Author

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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author

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
Copy link
Author

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
Copy link
Author 

[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
Copy link 

$ 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
Copy link

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)

@zhendongsu
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author 

[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
Copy link
Author

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 #6116 (comment)
@wintered

NikolajBjorner added a commit that referenced this issue Sep 19, 2022
@NikolajBjorner
bug fix for #6319
13f43ea 
literals that are replayed need to be registered with respective theories, otherwise, they will not propagate with the theories (the enode have to be attached with relevant theory variables).
NikolajBjorner added a commit that referenced this issue Sep 19, 2022
@NikolajBjorner
#6319
d6d34a8
NikolajBjorner added a commit that referenced this issue Sep 19, 2022
@NikolajBjorner
#6319
fce4d2a
NikolajBjorner added a commit that referenced this issue Sep 19, 2022
@NikolajBjorner
#6319
f4bea58 
ensure unknown when a lambda is not in beta redex
@merlinsun
Copy link

9118a93
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)

NikolajBjorner added a commit that referenced this issue Sep 20, 2022
@NikolajBjorner
#6319 resolve for unsat core when using assumptions
7caf6a6
@merlinsun
Copy link

A related instance about #6319 (comment)

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

NikolajBjorner added a commit that referenced this issue Sep 20, 2022
@NikolajBjorner
#6319
20250b2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@merlinsun
Copy link

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

NikolajBjorner added a commit that referenced this issue Sep 21, 2022
@NikolajBjorner
#6319
42945de 
align use of optsmt and the new core (they should not be used together)
@zhendongsu
Copy link
Author 

[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)

NikolajBjorner added a commit that referenced this issue Sep 23, 2022
@NikolajBjorner
#6319
c41b6da 
using a queue for disequality propagaiton was a regression: values of numerals can change along the same stack so prior passing the filter does not mean it passes later.
NikolajBjorner added a commit that referenced this issue Sep 24, 2022
@NikolajBjorner
#6319
1f150ec 
#6319 - fix incompleteness in propagation of default to all array terms in the equivalence class.

Fix bug with q_mbi where domain restrictions are not using values because the current model does not evaluate certain bound variables to values. Set model completion when adding these bound variables to the model to ensure their values are not missed.

Add better propagation of diagnostics when tactics and the new solver return unknown. The reason for unknown can now be traced to what theory was culprit (currently no additional information)
@zhendongsu
Copy link
Author 

[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
Copy link
Contributor

moving to #6364

@NikolajBjorner
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@NikolajBjorner @zhendongsu @wintered @merlinsun