File: fuzz01.smtv1.smt2

package info (click to toggle)
cvc4 1.8-2
links: PTS, VCS
area: main
in suites: bullseye
size: 69,876 kB
sloc: cpp: 274,686; sh: 5,833; python: 1,893; java: 929; lisp: 763; ansic: 275; perl: 214; makefile: 22; awk: 2
file content (10 lines) | stat: -rw-r--r-- 8,313 bytes
parent folder | download | duplicates (5)
(set-option :incremental false)
(set-info :status sat)
(set-logic QF_UFLRA)
(declare-fun f0 (Real) Real)
(declare-fun f1 (Real Real Real) Real)
(declare-fun p0 (Real Real Real) Bool)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(check-sat-assuming ( (let ((_let_0 (f0 v0))) (let ((_let_1 (ite (p0 v1 _let_0 v0) 1 0))) (let ((_let_2 (ite (p0 (/ _let_1 1) v1 v0) 1 0))) (let ((_let_3 (- _let_2 _let_2))) (let ((_let_4 (ite (p0 v0 (/ _let_1 1) v2) 1 0))) (let ((_let_5 (/ 0 2))) (let ((_let_6 (/ 2 2))) (let ((_let_7 (* (f1 v0 v1 v0) (/ (- 5) 1)))) (let ((_let_8 (< _let_1 _let_1))) (let ((_let_9 (<= v0 v1))) (let ((_let_10 (distinct _let_7 (- v0)))) (let ((_let_11 (> (- v1) (- v1)))) (let ((_let_12 (> _let_7 (/ _let_4 1)))) (let ((_let_13 (p0 (/ _let_4 1) (/ _let_4 1) _let_6))) (let ((_let_14 (distinct _let_0 (/ _let_4 1)))) (let ((_let_15 (= _let_7 v2))) (let ((_let_16 (>= (/ _let_2 1) (- v0)))) (let ((_let_17 (< (- v1) (/ _let_3 1)))) (let ((_let_18 (ite _let_12 _let_2 _let_6))) (let ((_let_19 (ite _let_12 _let_4 (f1 v0 v1 v0)))) (let ((_let_20 (ite _let_16 v1 _let_19))) (let ((_let_21 (ite _let_15 _let_3 (- v0)))) (let ((_let_22 (ite _let_10 _let_1 _let_7))) (let ((_let_23 (ite (<= _let_4 _let_4) v0 _let_4))) (let ((_let_24 (ite (distinct _let_5 (/ _let_4 1)) (ite (< v2 v0) (- v0) (- v1)) _let_6))) (let ((_let_25 (ite (> v2 v1) _let_7 _let_24))) (let ((_let_26 (ite (< v2 v0) (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2) (- v1)))) (let ((_let_27 (ite _let_8 (f1 v0 v1 v0) _let_2))) (let ((_let_28 (ite _let_9 (ite _let_16 _let_0 _let_6) v2))) (let ((_let_29 (ite _let_10 _let_2 _let_2))) (let ((_let_30 (ite (>= (/ _let_2 1) _let_5) _let_4 _let_6))) (let ((_let_31 (ite _let_8 _let_24 _let_0))) (let ((_let_32 (ite (p0 _let_0 (/ _let_4 1) _let_6) (ite _let_16 _let_0 _let_6) v2))) (let ((_let_33 (ite _let_12 _let_6 _let_25))) (let ((_let_34 (ite _let_8 _let_24 _let_33))) (let ((_let_35 (ite (< v2 v0) _let_23 _let_4))) (let ((_let_36 (ite (= _let_5 (/ _let_4 1)) v1 _let_18))) (let ((_let_37 (ite (p0 _let_7 _let_5 (- v1)) _let_7 _let_32))) (let ((_let_38 (ite (<= _let_4 _let_4) _let_33 _let_18))) (let ((_let_39 (ite _let_13 _let_30 _let_25))) (let ((_let_40 (ite (= (or (not (=> (=> (<= (ite (<= _let_4 _let_4) (- v0) _let_2) _let_30) (>= _let_32 _let_18)) (> v2 v1))) (=> (ite (and (>= (ite _let_11 (ite _let_17 _let_26 v2) _let_26) (/ _let_1 1)) (> _let_39 _let_26)) (ite (= (and (not (>= _let_30 (ite _let_16 _let_0 _let_6))) (and (p0 _let_32 _let_30 _let_34) (= _let_26 (ite (< v2 v0) (- v0) (- v1))))) (xor (< _let_20 (/ _let_4 1)) (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)))) (=> (ite (and (=> (= (/ _let_4 1) _let_33) _let_8) (p0 _let_33 _let_27 v1)) (ite (>= _let_6 _let_25) (p0 _let_0 (/ _let_4 1) _let_6) (= _let_30 (ite _let_16 _let_0 _let_6))) (distinct _let_5 (/ _let_4 1))) (or (distinct v2 _let_6) (<= _let_30 (/ _let_3 1)))) (and (< _let_24 _let_20) (ite (<= (ite _let_16 _let_0 _let_6) _let_25) (ite (< _let_36 _let_5) (>= v2 (/ _let_3 1)) (>= _let_38 v1)) _let_13))) (not (= (= (ite _let_17 _let_26 v2) (ite _let_14 _let_6 (ite _let_16 _let_0 _let_6))) (= (ite _let_17 _let_26 v2) (ite _let_14 _let_6 (ite _let_16 _let_0 _let_6)))))) (< _let_26 (- v1)))) (= (=> (xor (=> (or (= (= v1 _let_6) (ite (= _let_26 _let_35) (distinct _let_26 _let_28) (< _let_5 _let_37))) (and (= _let_11 (not (>= (/ _let_2 1) _let_5))) (< _let_34 _let_22))) (xor (or (p0 _let_38 v2 v1) (distinct (/ _let_4 1) _let_31)) (= (< _let_19 _let_23) (= (xor (= _let_22 _let_31) (or (p0 (f1 v0 v1 v0) _let_24 (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2)) (<= (/ _let_4 1) (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2)))) (> _let_32 _let_39))))) (ite (> v0 (/ _let_4 1)) (< (- v1) _let_18) (and (= (<= v1 (ite (= v0 (- v1)) _let_5 _let_5)) (distinct v0 (ite (distinct (/ _let_4 1) (- v0)) _let_23 _let_24))) (= (<= v1 (ite (= v0 (- v1)) _let_5 _let_5)) (distinct v0 (ite (distinct (/ _let_4 1) (- v0)) _let_23 _let_24)))))) (ite (xor (= (and (= _let_24 (/ _let_4 1)) (p0 _let_23 _let_25 (f1 v0 v1 v0))) (distinct (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2) (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2))) (distinct _let_27 _let_6)) (not (xor (>= (/ _let_29 1) _let_7) (= (and (= _let_14 (> _let_30 (/ _let_29 1))) (< _let_22 _let_19)) (not (ite (= _let_5 _let_6) _let_16 (= _let_17 _let_15)))))) (=> (> _let_3 _let_3) (or (>= (/ _let_3 1) v1) (=> (p0 (/ _let_1 1) _let_37 _let_21) (<= (/ _let_2 1) _let_6)))))) (> _let_31 _let_5))) (not (or (xor (and (or (not (xor (ite (or _let_10 (p0 (f1 v0 v1 v0) (/ _let_1 1) (ite (< v2 v0) (- v0) (- v1)))) (p0 _let_28 (/ _let_4 1) _let_23) (>= _let_24 _let_7)) (<= _let_31 _let_6))) (not (and (<= (ite (distinct (/ _let_4 1) (- v0)) _let_23 _let_24) (/ _let_1 1)) (= (=> (= v0 (- v1)) (not (> (ite (distinct (/ _let_4 1) (- v0)) _let_23 _let_24) (/ _let_29 1)))) (xor (p0 _let_37 (ite (< v2 v0) (- v0) (- v1)) _let_34) (xor (<= _let_4 _let_4) (distinct (ite (= v0 (- v1)) _let_5 _let_5) _let_33))))))) (>= _let_34 (/ _let_29 1))) (=> (and (not (> _let_19 _let_0)) (>= (ite _let_14 _let_6 (ite _let_16 _let_0 _let_6)) (- v0))) (=> (or (>= v0 (ite _let_16 _let_0 _let_6)) (>= (/ _let_4 1) (f1 v0 v1 v0))) (<= _let_19 _let_32)))) (and (xor (ite (or (= _let_5 (/ _let_4 1)) (= (ite (< v2 v0) (- v0) (- v1)) (- v1))) (p0 _let_7 _let_5 (- v1)) (xor (p0 _let_22 _let_19 _let_36) (or (= v2 (- v0)) (< v2 v0)))) (=> (= (> (ite (= v0 (- v1)) _let_5 _let_5) _let_21) (= (>= (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2) _let_35) _let_9)) (xor (p0 (ite (= v0 (- v1)) _let_5 _let_5) (/ _let_4 1) _let_35) (xor (distinct _let_37 (- v0)) (p0 v2 _let_32 _let_34))))) (=> (= (or (p0 _let_36 _let_32 (ite (distinct (/ _let_4 1) (- v0)) _let_23 _let_24)) (and (xor (distinct _let_27 (ite (< v2 v0) (- v0) (- v1))) (>= _let_37 v0)) (p0 _let_32 (/ _let_29 1) (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2)))) (<= _let_27 _let_23)) _let_12)))) (= (or (not (=> (=> (<= (ite (<= _let_4 _let_4) (- v0) _let_2) _let_30) (>= _let_32 _let_18)) (> v2 v1))) (=> (ite (and (>= (ite _let_11 (ite _let_17 _let_26 v2) _let_26) (/ _let_1 1)) (> _let_39 _let_26)) (ite (= (and (not (>= _let_30 (ite _let_16 _let_0 _let_6))) (and (p0 _let_32 _let_30 _let_34) (= _let_26 (ite (< v2 v0) (- v0) (- v1))))) (xor (< _let_20 (/ _let_4 1)) (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)))) (=> (ite (and (=> (= (/ _let_4 1) _let_33) _let_8) (p0 _let_33 _let_27 v1)) (ite (>= _let_6 _let_25) (p0 _let_0 (/ _let_4 1) _let_6) (= _let_30 (ite _let_16 _let_0 _let_6))) (distinct _let_5 (/ _let_4 1))) (or (distinct v2 _let_6) (<= _let_30 (/ _let_3 1)))) (and (< _let_24 _let_20) (ite (<= (ite _let_16 _let_0 _let_6) _let_25) (ite (< _let_36 _let_5) (>= v2 (/ _let_3 1)) (>= _let_38 v1)) _let_13))) (not (= (= (ite _let_17 _let_26 v2) (ite _let_14 _let_6 (ite _let_16 _let_0 _let_6))) (= (ite _let_17 _let_26 v2) (ite _let_14 _let_6 (ite _let_16 _let_0 _let_6)))))) (< _let_26 (- v1)))) (= (=> (xor (=> (or (= (= v1 _let_6) (ite (= _let_26 _let_35) (distinct _let_26 _let_28) (< _let_5 _let_37))) (and (= _let_11 (not (>= (/ _let_2 1) _let_5))) (< _let_34 _let_22))) (xor (or (p0 _let_38 v2 v1) (distinct (/ _let_4 1) _let_31)) (= (< _let_19 _let_23) (= (xor (= _let_22 _let_31) (or (p0 (f1 v0 v1 v0) _let_24 (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2)) (<= (/ _let_4 1) (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2)))) (> _let_32 _let_39))))) (ite (> v0 (/ _let_4 1)) (< (- v1) _let_18) (and (= (<= v1 (ite (= v0 (- v1)) _let_5 _let_5)) (distinct v0 (ite (distinct (/ _let_4 1) (- v0)) _let_23 _let_24))) (= (<= v1 (ite (= v0 (- v1)) _let_5 _let_5)) (distinct v0 (ite (distinct (/ _let_4 1) (- v0)) _let_23 _let_24)))))) (ite (xor (= (and (= _let_24 (/ _let_4 1)) (p0 _let_23 _let_25 (f1 v0 v1 v0))) (distinct (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2) (ite (p0 (/ _let_2 1) v1 (f1 v0 v1 v0)) v1 v2))) (distinct _let_27 _let_6)) (not (xor (>= (/ _let_29 1) _let_7) (= (and (= _let_14 (> _let_30 (/ _let_29 1))) (< _let_22 _let_19)) (not (ite (= _let_5 _let_6) _let_16 (= _let_17 _let_15)))))) (=> (> _let_3 _let_3) (or (>= (/ _let_3 1) v1) (=> (p0 (/ _let_1 1) _let_37 _let_21) (<= (/ _let_2 1) _let_6)))))) (> _let_31 _let_5)))))) (= (and (distinct (/ _let_4 1) (- v0)) (> (ite (= v0 (- v1)) _let_5 _let_5) (/ _let_1 1))) (xor _let_40 _let_40))))))))))))))))))))))))))))))))))))))))))) ))