Skip to content

heap-use-after-free at util/mpz.h:448 #4110

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
Closed
rainoftime opened this issue Apr 26, 2020 · 1 comment
Closed

heap-use-after-free at util/mpz.h:448 #4110

rainoftime opened this issue Apr 26, 2020 · 1 comment

Comments

@rainoftime
Copy link
Contributor

rainoftime commented Apr 26, 2020 •
edited
Loading

Hi, for the following formula,
uaf.txt

z3 (commit 7f1b147) throw a uaf

sat
=================================================================
==45471==ERROR: AddressSanitizer: heap-use-after-free on address 0x607000343b88 at pc 0x000000563c60 bp 0x7fffb77c5eb0 sp 0x7fffb77c5ea0
READ of size 4 at 0x607000343b88 thread T0
    #0 0x563c5f in mpz_manager<false>::sign(mpz const&) ../src/util/mpz.h:448
    #1 0x5629fe in mpz_manager<false>::is_neg(mpz const&) ../src/util/mpz.h:442
    #2 0xc54c4e in mpz_manager<false>::is_nonneg(mpz const&) ../src/util/mpz.h:459
    #3 0x249d3f1 in mpbq_manager::is_nonneg(mpbq const&) const ../src/util/mpbq.h:99
    #4 0x25475e5 in algebraic_numbers::manager::imp::magnitude(mpbq const&, mpbq const&) ../src/math/polynomial/algebraic_numbers.cpp:744
    #5 0x25477ca in algebraic_numbers::manager::imp::magnitude(algebraic_numbers::algebraic_cell*) ../src/math/polynomial/algebraic_numbers.cpp:759
    #6 0x2548d42 in algebraic_numbers::manager::imp::save_intervals::restore_if_too_small() ../src/math/polynomial/algebraic_numbers.cpp:968
    #7 0x2548c00 in algebraic_numbers::manager::imp::save_intervals::~save_intervals() ../src/math/polynomial/algebraic_numbers.cpp:958
    #8 0x2543381 in algebraic_numbers::manager::imp::is_rational(algebraic_numbers::anum&) ../src/math/polynomial/algebraic_numbers.cpp:295
    #9 0x253d4b6 in algebraic_numbers::manager::is_rational(algebraic_numbers::anum const&) ../src/math/polynomial/algebraic_numbers.cpp:2887
    #10 0x1fb9d03 in nlsat::interval_set_manager::peek_in_complement(nlsat::interval_set const*, bool, algebraic_numbers::anum&, bool) ../src/nlsat/nlsat_interval_set.cpp:751
    #11 0x1f8973d in nlsat::solver::imp::select_witness() ../src/nlsat/nlsat_solver.cpp:1454
    #12 0x1f8ad8b in nlsat::solver::imp::search() ../src/nlsat/nlsat_solver.cpp:1536
    #13 0x1f8af4d in nlsat::solver::imp::search_check() ../src/nlsat/nlsat_solver.cpp:1545
    #14 0x1f8bf9b in nlsat::solver::imp::check() ../src/nlsat/nlsat_solver.cpp:1619
    #15 0x1f78239 in nlsat::solver::check() ../src/nlsat/nlsat_solver.cpp:3484
    #16 0x16a6bf1 in nlsat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/nlsat/tactic/nlsat_tactic.cpp:159
    #17 0x16a7740 in nlsat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/nlsat/tactic/nlsat_tactic.cpp:241
    #18 0x1a65773 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:918
    #19 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #20 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #21 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #22 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #23 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #24 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #25 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #26 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #27 0x1a65b13 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:942
    #28 0x1a5f867 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:296
    #29 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #30 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #31 0x1a66b10 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1032
    #32 0x1a66b7a in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #33 0x1a66b7a in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #34 0x1a66b7a in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #35 0x1a66b7a in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #36 0x1a66b7a in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #37 0x1a66b7a in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #38 0x1a5e465 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #39 0x1a6411d in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:769
    #40 0x1a58a68 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #41 0x1a58f03 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:168
    #42 0x19def58 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
    #43 0x19e40f5 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
@rainoftime
Copy link
Contributor Author

A smaller case

set-logic QF_UFNRA)
(set-option :rewriter.eq2ineq true)
(set-option :rewriter.arith_ineq_lhs true)
(set-option :rewriter.elim_and true)
(set-option :algebraic.factor false)
(set-option :rewriter.sort_sums true)
(set-option :nlsat.shuffle_vars true)
(set-option :smt.arith.solver 5)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const r0 Real)
(declare-const v7 Bool)
(declare-const r1 Real)
(declare-const v8 Bool)
(declare-const r2 Real)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const v13 Bool)
(declare-const r5 Real)
(declare-const r6 Real)
(declare-const v14 Bool)
(declare-const r7 Real)
(declare-const v15 Bool)
(declare-const v16 Bool)
(assert (or (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r2) v0 (or v10 v13 (xor v13 v14 (<= r0 r0 (/ r0 r0) r0) (not v10) v15 (= (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r1 (- (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2))) (<= r0 (* (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (- (/ r0 r0)) r3) r2) r3) (distinct (/ r0 r0) (/ r0 r0) (/ r0 r0))) (> (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) r1 r1 r0) v16 (distinct v2 (> 0.0 r1 r1 r0) (distinct v7 v1) v2 (>= r4 (- r0 0.0 0.0 (- 0.0)) (+ r2 (- r0 (* (- 0.0) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) r1 0.0) (> 0.0 r2 0.0) (or (distinct v7 v1) (<= r1 (- r0 (* 0.0 r1 0.0 r0 r0) (- (/ r0 r0)) (- (/ r0 r0)))) (> (/ r0 r0) r0 r0 (/ r0 r0) r0)) (distinct r0 r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (and v3 v3 (distinct (/ r0 r0) (/ r0 r0) (/ r0 r0)) v7 v1)) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (distinct v7 v1) (distinct r0 r0) (> (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) r2) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) 0.0))))
(assert (or v2 v0 (>= 0.0 r3 0.0 0.0 r7)))
(assert (or v0 (or v10 v13 (xor v13 v14 (<= r0 r0 (/ r0 r0) r0) (not v10) v15 (= (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r1 0.0) (<= r0 (* (- r0 (* (- 0.0) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (- (/ r0 r0)) r3) r2) r3) (distinct (/ r0 r0) (/ r0 r0) (/ r0 r0))) (> (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) r1 r1 r0) v16 (distinct v2 (> (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) r1 r1 r0) (distinct v7 v1) v2 (>= r4 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) r1 (+ r2 0.0 0.0 (+ 0.0 (- 0.0) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2)) (> (/ r0 r0) r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (or (distinct v7 v1) (<= r1 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0)))) (> (/ r0 r0) r0 r0 (/ r0 r0) r0)) (distinct r0 r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (and v3 v3 (distinct (/ r0 r0) (/ r0 r0) (/ r0 r0)) v7 v1)) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (distinct v7 v1) (distinct r0 r0) (> (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) r2) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) 0.0 (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) 0.0)) (<= 0.0 0.0 9.232216 (* r0 0.0) (- (- (/ r0 r0))))))
(assert (or (or v10 v13 (xor v13 v14 (<= r0 r0 0.0 r0) (not v10) v15 (= 0.0 r1 0.0) (<= r0 0.0 r3) (distinct 0.0 0.0 0.0)) (> 0.0 r1 r1 r0) v16 (distinct v2 (> 0.0 r1 r1 r0) (distinct v7 v1) v2 (>= r4 0.0 0.0 r1 (+ r2 (- r0 0.0 0.0 (- 0.0)) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2)) (> (/ r0 r0) r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (or (distinct v7 v1) (<= r1 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0)))) (> (/ r0 r0) r0 r0 (/ r0 r0) r0)) (distinct r0 r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (and v3 v3 (distinct (/ r0 r0) (/ r0 r0) (/ r0 r0)) v7 v1)) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) 0.0 0.0) (distinct v7 v1) (distinct r0 r0) (> (+ 0.0 0.0 r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) 0.0 r2) (<= 0.0 (- r0 (* 0.0 r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)))) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r2) (<= (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) 9.232216 (* r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- (- (/ r0 r0))))))
(assert (or (>= (- r1) r3 (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (/ r0 r0) r7) (distinct 0.0 r2) (distinct 0.0 r2)))
(assert (or (> (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (> 0.0 (/ 0.0 (* 0.0 r1 0.0 r0 r0))) (<= (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) 0.0 9.232216 0.0 0.0)))
(assert (or (>= 0.0 r3 0.0 0.0 r7) (> (+ r2 0.0 0.0 (+ 0.0 0.0 r0 (+ r2 0.0)) r2) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (<= (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) 9.232216 (* r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- (- (/ r0 r0))))))
(assert (or (or v10 v13 (xor v13 v14 (<= r0 r0 (/ r0 r0) r0) (not v10) v15 (= 0.0 r1 0.0) (<= r0 0.0 r3) (distinct 0.0 0.0 0.0)) (> (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) r1 r1 r0) v16 (distinct v2 (> (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) r1 r1 r0) (distinct v7 v1) v2 (>= r4 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* 0.0 r1 (/ r0 r0) r0 r0))) r2) r1 0.0) (> 0.0 r2 0.0) (or (distinct v7 v1) (<= r1 (- r0 (* 0.0 r1 (/ r0 r0) r0 r0) 0.0 (- 0.0))) (> (/ r0 r0) r0 r0 (/ r0 r0) r0)) (distinct r0 r0) (distinct (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) r0) (distinct 0.0 r0) (and v3 v3 (distinct 0.0 0.0 0.0) v7 v1)) (<= 0.0 (- r0 0.0 0.0 0.0) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (distinct v7 v1) (distinct r0 r0) (> (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) (+ r2 (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (+ (/ r0 r0) (- (/ r0 r0)) r0 (+ r2 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0))) r2) r2) (<= (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (- r0 (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0) (- (/ r0 r0)) (- (/ r0 r0))) (/ (/ r0 r0) (* (- (/ r0 r0)) r1 (/ r0 r0) r0 r0)))) (distinct 0.0 r2) v2))
(check-sat)
(check-sat)

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
1 participant
@rainoftime