Commit 92b62a51 authored by Alain Mebsout's avatar Alain Mebsout
Browse files

Importing snapshot 2015-06-01

parents
Pipeline #12 skipped
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
no description
\ No newline at end of file
(set-logic QF_ALIA)
(set-info :source |
Benchmarks from Leonardo de Moura <demoura@csl.sri.com>
This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Int)
(declare-fun x_1 () Int)
(declare-fun x_2 () (Array Int Int))
(declare-fun x_3 () Int)
(declare-fun x_4 () (Array Int Int))
(declare-fun x_5 () Int)
(declare-fun x_6 () Int)
(declare-fun x_7 () Int)
(declare-fun x_8 () Int)
(declare-fun x_9 () Int)
(declare-fun x_10 () (Array Int Int))
(declare-fun x_11 () Int)
(declare-fun x_12 () Int)
(declare-fun x_13 () Int)
(declare-fun x_14 () (Array Int Int))
(declare-fun x_15 () Int)
(declare-fun x_16 () Int)
(declare-fun x_17 () Int)
(declare-fun x_18 () (Array Int Int))
(declare-fun x_19 () Int)
(declare-fun x_20 () Int)
(declare-fun x_21 () Int)
(declare-fun x_22 () (Array Int Int))
(declare-fun x_23 () Int)
(declare-fun x_24 () Int)
(declare-fun x_25 () Int)
(declare-fun x_26 () (Array Int Int))
(declare-fun x_27 () Int)
(declare-fun x_28 () Int)
(declare-fun x_29 () Int)
(declare-fun x_30 () (Array Int Int))
(declare-fun x_31 () Int)
(declare-fun x_32 () Int)
(declare-fun x_33 () Int)
(declare-fun x_34 () Int)
(declare-fun x_35 () (Array Int Int))
(declare-fun x_36 () Int)
(declare-fun x_37 () (Array Int Int))
(declare-fun x_38 () Int)
(declare-fun x_39 () (Array Int Int))
(declare-fun x_40 () Int)
(declare-fun x_41 () (Array Int Int))
(declare-fun x_42 () Int)
(declare-fun x_43 () (Array Int Int))
(declare-fun x_44 () Int)
(assert (let ((?v_5 (= x_9 1)) (?v_3 (= x_17 1)) (?v_0 (= x_29 1)) (?v_6 (= x_3 0)) (?v_2 (= x_21 1)) (?v_1 (= x_25 1)) (?v_4 (= x_13 1)) (?v_7 (store x_43 x_32 (select x_30 x_31)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_33 2) (>= x_33 0)) (<= x_29 2)) (>= x_29 0)) (<= x_25 2)) (>= x_25 0)) (<= x_21 2)) (>= x_21 0)) (<= x_17 2)) (>= x_17 0)) (<= x_13 2)) (>= x_13 0)) (<= x_9 2)) (>= x_9 0)) (not (< x_0 0))) (not (< x_1 0))) (not (< x_3 0))) (not (< x_11 0))) (not (< x_12 0))) (not (< x_15 0))) (not (< x_16 0))) (not (< x_19 0))) (not (< x_20 0))) (not (< x_23 0))) (not (< x_24 0))) (not (< x_27 0))) (not (< x_28 0))) (not (< x_31 0))) (not (< x_32 0))) (not (< x_34 0))) (not (< x_36 0))) (not (< x_38 0))) (not (< x_40 0))) (not (< x_42 0))) (not (< x_44 0))) (= x_0 0)) (= x_1 0)) ?v_6) (= x_33 (ite (<= x_32 2) 1 (ite (<= x_32 5) 0 2)))) (= x_29 (ite (<= x_28 2) 1 (ite (<= x_28 5) 0 2)))) (= x_25 (ite (<= x_24 2) 1 (ite (<= x_24 5) 0 2)))) (= x_21 (ite (<= x_20 2) 1 (ite (<= x_20 5) 0 2)))) (= x_17 (ite (<= x_16 2) 1 (ite (<= x_16 5) 0 2)))) (= x_13 (ite (<= x_12 2) 1 (ite (<= x_12 5) 0 2)))) (= (select x_4 0) (select x_2 x_0))) (= x_9 (ite (<= x_3 2) 1 (ite (<= x_3 5) 0 2)))) (= x_31 (ite (= x_29 0) (+ x_27 1) x_27))) (= x_44 (ite ?v_0 (+ x_42 1) x_42))) (= x_30 (ite ?v_0 (store x_26 x_42 (ite (= x_28 0) x_5 (ite (= x_28 1) x_6 (ite (= x_28 2) x_7 x_8)))) x_26))) (= x_32 (+ x_28 1))) (= x_27 (ite (= x_25 0) (+ x_23 1) x_23))) (= x_42 (ite ?v_1 (+ x_40 1) x_40))) (= x_26 (ite ?v_1 (store x_22 x_40 (ite (= x_24 0) x_5 (ite (= x_24 1) x_6 (ite (= x_24 2) x_7 x_8)))) x_22))) (= x_28 (+ x_24 1))) (= x_43 (store x_41 x_28 (select x_26 x_27)))) (= x_23 (ite (= x_21 0) (+ x_19 1) x_19))) (= x_40 (ite ?v_2 (+ x_38 1) x_38))) (= x_22 (ite ?v_2 (store x_18 x_38 (ite (= x_20 0) x_5 (ite (= x_20 1) x_6 (ite (= x_20 2) x_7 x_8)))) x_18))) (= x_24 (+ x_20 1))) (= x_41 (store x_39 x_24 (select x_22 x_23)))) (= x_19 (ite (= x_17 0) (+ x_15 1) x_15))) (= x_38 (ite ?v_3 (+ x_36 1) x_36))) (= x_18 (ite ?v_3 (store x_14 x_36 (ite (= x_16 0) x_5 (ite (= x_16 1) x_6 (ite (= x_16 2) x_7 x_8)))) x_14))) (= x_20 (+ x_16 1))) (= x_39 (store x_37 x_20 (select x_18 x_19)))) (= x_15 (ite (= x_13 0) (+ x_11 1) x_11))) (= x_36 (ite ?v_4 (+ x_34 1) x_34))) (= x_14 (ite ?v_4 (store x_10 x_34 (ite (= x_12 0) x_5 (ite (= x_12 1) x_6 (ite (= x_12 2) x_7 x_8)))) x_10))) (= x_16 (+ x_12 1))) (= x_37 (store x_35 x_16 (select x_14 x_15)))) (= x_11 (ite (= x_9 0) (+ x_0 1) x_0))) (= x_34 (ite ?v_5 (+ x_1 1) x_1))) (= x_10 (ite ?v_5 (store x_2 x_1 (ite ?v_6 x_5 (ite (= x_3 1) x_6 (ite (= x_3 2) x_7 x_8)))) x_2))) (= x_12 (+ x_3 1))) (= x_35 (store x_4 x_12 (select x_10 x_11)))) (or (or (or (or (or (or (and (not (< x_32 6)) (or (or (not (= (select ?v_7 3) x_5)) (not (= (select ?v_7 4) x_6))) (not (= (select ?v_7 5) x_7)))) (and (not (< x_28 6)) (or (or (not (= (select x_43 3) x_5)) (not (= (select x_43 4) x_6))) (not (= (select x_43 5) x_7))))) (and (not (< x_24 6)) (or (or (not (= (select x_41 3) x_5)) (not (= (select x_41 4) x_6))) (not (= (select x_41 5) x_7))))) (and (not (< x_20 6)) (or (or (not (= (select x_39 3) x_5)) (not (= (select x_39 4) x_6))) (not (= (select x_39 5) x_7))))) (and (not (< x_16 6)) (or (or (not (= (select x_37 3) x_5)) (not (= (select x_37 4) x_6))) (not (= (select x_37 5) x_7))))) (and (not (< x_12 6)) (or (or (not (= (select x_35 3) x_5)) (not (= (select x_35 4) x_6))) (not (= (select x_35 5) x_7))))) (and (not (< x_3 6)) (or (or (not (= (select x_4 3) x_5)) (not (= (select x_4 4) x_6))) (not (= (select x_4 5) x_7))))))))
(check-sat)
(exit)
(set-logic QF_ALIA)
(set-info :source |
Benchmarks from Leonardo de Moura <demoura@csl.sri.com>
This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Int)
(declare-fun x_1 () Int)
(declare-fun x_2 () (Array Int Int))
(declare-fun x_3 () Int)
(declare-fun x_4 () (Array Int Int))
(declare-fun x_5 () Int)
(declare-fun x_6 () Int)
(declare-fun x_7 () Int)
(declare-fun x_8 () Int)
(declare-fun x_9 () Int)
(declare-fun x_10 () Int)
(declare-fun x_11 () (Array Int Int))
(declare-fun x_12 () Int)
(declare-fun x_13 () Int)
(declare-fun x_14 () Int)
(declare-fun x_15 () (Array Int Int))
(declare-fun x_16 () Int)
(declare-fun x_17 () Int)
(declare-fun x_18 () Int)
(declare-fun x_19 () (Array Int Int))
(declare-fun x_20 () Int)
(declare-fun x_21 () Int)
(declare-fun x_22 () Int)
(declare-fun x_23 () (Array Int Int))
(declare-fun x_24 () Int)
(declare-fun x_25 () Int)
(declare-fun x_26 () Int)
(declare-fun x_27 () (Array Int Int))
(declare-fun x_28 () Int)
(declare-fun x_29 () Int)
(declare-fun x_30 () Int)
(declare-fun x_31 () (Array Int Int))
(declare-fun x_32 () Int)
(declare-fun x_33 () Int)
(declare-fun x_34 () Int)
(declare-fun x_35 () Int)
(declare-fun x_36 () Int)
(declare-fun x_37 () (Array Int Int))
(declare-fun x_38 () Int)
(declare-fun x_39 () Int)
(declare-fun x_40 () (Array Int Int))
(declare-fun x_41 () Int)
(declare-fun x_42 () Int)
(declare-fun x_43 () (Array Int Int))
(declare-fun x_44 () Int)
(declare-fun x_45 () Int)
(declare-fun x_46 () (Array Int Int))
(declare-fun x_47 () Int)
(declare-fun x_48 () Int)
(declare-fun x_49 () (Array Int Int))
(declare-fun x_50 () Int)
(declare-fun x_51 () Int)
(assert (let ((?v_3 (= x_47 1)) (?v_14 (<= x_16 x_39)) (?v_25 (= x_5 1)) (?v_17 (= x_14 1)) (?v_11 (= x_41 1)) (?v_13 (= x_18 1)) (?v_1 (<= x_28 x_48)) (?v_22 (= x_3 0)) (?v_12 (= x_44 0)) (?v_21 (= x_10 1)) (?v_16 (= x_41 0)) (?v_0 (= x_30 1)) (?v_19 (= x_35 1)) (?v_18 (<= x_12 x_36)) (?v_20 (= x_38 0)) (?v_4 (= x_50 0)) (?v_2 (= x_50 1)) (?v_8 (= x_47 0)) (?v_26 (= x_35 0)) (?v_15 (= x_38 1)) (?v_24 (<= x_0 x_1)) (?v_10 (<= x_20 x_42)) (?v_9 (= x_22 1)) (?v_7 (= x_44 1)) (?v_6 (<= x_24 x_45)) (?v_5 (= x_26 1)) (?v_23 (= x_5 2)) (?v_27 (= x_5 0))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_34 2) (>= x_34 0)) (<= x_30 2)) (>= x_30 0)) (<= x_26 2)) (>= x_26 0)) (<= x_22 2)) (>= x_22 0)) (<= x_18 2)) (>= x_18 0)) (<= x_14 2)) (>= x_14 0)) (<= x_10 2)) (>= x_10 0)) (not (< x_0 0))) (not (< x_1 0))) (not (< x_3 0))) (not (< x_5 0))) (<= x_5 2)) (not (< x_12 0))) (not (< x_13 0))) (not (< x_16 0))) (not (< x_17 0))) (not (< x_20 0))) (not (< x_21 0))) (not (< x_24 0))) (not (< x_25 0))) (not (< x_28 0))) (not (< x_29 0))) (not (< x_32 0))) (not (< x_33 0))) (not (< x_35 0))) (<= x_35 2)) (not (< x_36 0))) (not (< x_38 0))) (<= x_38 2)) (not (< x_39 0))) (not (< x_41 0))) (<= x_41 2)) (not (< x_42 0))) (not (< x_44 0))) (<= x_44 2)) (not (< x_45 0))) (not (< x_47 0))) (<= x_47 2)) (not (< x_48 0))) (not (< x_50 0))) (<= x_50 2)) (not (< x_51 0))) (= x_0 0)) (= x_1 0)) ?v_22) ?v_23) (= x_34 (ite (<= x_33 2) 1 (ite (<= x_33 5) 0 2)))) (= x_30 (ite (<= x_29 2) 1 (ite (<= x_29 5) 0 2)))) (= x_26 (ite (<= x_25 2) 1 (ite (<= x_25 5) 0 2)))) (= x_22 (ite (<= x_21 2) 1 (ite (<= x_21 5) 0 2)))) (= x_18 (ite (<= x_17 2) 1 (ite (<= x_17 5) 0 2)))) (= x_14 (ite (<= x_13 2) 1 (ite (<= x_13 5) 0 2)))) (= (select x_4 0) (select x_2 x_0))) (= x_10 (ite (<= x_3 2) 1 (ite (<= x_3 5) 0 2)))) (= x_32 (ite (= x_30 0) (+ x_28 1) x_28))) (= x_51 (ite ?v_0 (+ x_48 1) x_48))) (= x_31 (ite ?v_0 (store x_27 x_48 (ite (= x_29 0) x_6 (ite (= x_29 1) x_7 (ite (= x_29 2) x_8 x_9)))) x_27))) (= x_33 (+ x_29 1))) (or (or (or (and (and (= x_47 2) ?v_1) ?v_2) (and (and ?v_3 ?v_1) ?v_2)) (and (and ?v_3 (not ?v_1)) ?v_4)) (and ?v_8 ?v_4))) (= x_28 (ite (= x_26 0) (+ x_24 1) x_24))) (= x_48 (ite ?v_5 (+ x_45 1) x_45))) (= x_27 (ite ?v_5 (store x_23 x_45 (ite (= x_25 0) x_6 (ite (= x_25 1) x_7 (ite (= x_25 2) x_8 x_9)))) x_23))) (= x_29 (+ x_25 1))) (= x_49 (store x_46 x_29 (select x_27 x_28)))) (or (or (or (and (and (= x_44 2) ?v_6) ?v_3) (and (and ?v_7 ?v_6) ?v_3)) (and (and ?v_7 (not ?v_6)) ?v_8)) (and ?v_12 ?v_8))) (= x_24 (ite (= x_22 0) (+ x_20 1) x_20))) (= x_45 (ite ?v_9 (+ x_42 1) x_42))) (= x_23 (ite ?v_9 (store x_19 x_42 (ite (= x_21 0) x_6 (ite (= x_21 1) x_7 (ite (= x_21 2) x_8 x_9)))) x_19))) (= x_25 (+ x_21 1))) (= x_46 (store x_43 x_25 (select x_23 x_24)))) (or (or (or (and (and (= x_41 2) ?v_10) ?v_7) (and (and ?v_11 ?v_10) ?v_7)) (and (and ?v_11 (not ?v_10)) ?v_12)) (and ?v_16 ?v_12))) (= x_20 (ite (= x_18 0) (+ x_16 1) x_16))) (= x_42 (ite ?v_13 (+ x_39 1) x_39))) (= x_19 (ite ?v_13 (store x_15 x_39 (ite (= x_17 0) x_6 (ite (= x_17 1) x_7 (ite (= x_17 2) x_8 x_9)))) x_15))) (= x_21 (+ x_17 1))) (= x_43 (store x_40 x_21 (select x_19 x_20)))) (or (or (or (and (and (= x_38 2) ?v_14) ?v_11) (and (and ?v_15 ?v_14) ?v_11)) (and (and ?v_15 (not ?v_14)) ?v_16)) (and ?v_20 ?v_16))) (= x_16 (ite (= x_14 0) (+ x_12 1) x_12))) (= x_39 (ite ?v_17 (+ x_36 1) x_36))) (= x_15 (ite ?v_17 (store x_11 x_36 (ite (= x_13 0) x_6 (ite (= x_13 1) x_7 (ite (= x_13 2) x_8 x_9)))) x_11))) (= x_17 (+ x_13 1))) (= x_40 (store x_37 x_17 (select x_15 x_16)))) (or (or (or (and (and (= x_35 2) ?v_18) ?v_15) (and (and ?v_19 ?v_18) ?v_15)) (and (and ?v_19 (not ?v_18)) ?v_20)) (and ?v_26 ?v_20))) (= x_12 (ite (= x_10 0) (+ x_0 1) x_0))) (= x_36 (ite ?v_21 (+ x_1 1) x_1))) (= x_11 (ite ?v_21 (store x_2 x_1 (ite ?v_22 x_6 (ite (= x_3 1) x_7 (ite (= x_3 2) x_8 x_9)))) x_2))) (= x_13 (+ x_3 1))) (= x_37 (store x_4 x_13 (select x_11 x_12)))) (or (or (or (and (and ?v_23 ?v_24) ?v_19) (and (and ?v_25 ?v_24) ?v_19)) (and (and ?v_25 (not ?v_24)) ?v_26)) (and ?v_27 ?v_26))) (or (or (or (or (or (or ?v_4 ?v_8) ?v_12) ?v_16) ?v_20) ?v_26) ?v_27))))
(check-sat)
(exit)
(set-logic QF_ALIA)
(set-info :source |
Benchmarks from Leonardo de Moura <demoura@csl.sri.com>
This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Int)
(declare-fun x_1 () (Array Int Int))
(declare-fun x_2 () Int)
(declare-fun x_3 () (Array Int Int))
(declare-fun x_4 () Int)
(declare-fun x_5 () Int)
(declare-fun x_6 () Int)
(declare-fun x_7 () Int)
(declare-fun x_8 () Int)
(declare-fun x_9 () Int)
(declare-fun x_10 () Int)
(declare-fun x_11 () (Array Int Int))
(declare-fun x_12 () Int)
(declare-fun x_13 () Int)
(declare-fun x_14 () Int)
(declare-fun x_15 () (Array Int Int))
(declare-fun x_16 () Int)
(declare-fun x_17 () Int)
(declare-fun x_18 () Int)
(declare-fun x_19 () (Array Int Int))
(declare-fun x_20 () Int)
(declare-fun x_21 () Int)
(declare-fun x_22 () Int)
(declare-fun x_23 () (Array Int Int))
(declare-fun x_24 () Int)
(declare-fun x_25 () Int)
(declare-fun x_26 () Int)
(declare-fun x_27 () (Array Int Int))
(declare-fun x_28 () Int)
(declare-fun x_29 () Int)
(declare-fun x_30 () Int)
(declare-fun x_31 () (Array Int Int))
(declare-fun x_32 () Int)
(declare-fun x_33 () Int)
(declare-fun x_34 () (Array Int Int))
(declare-fun x_35 () (Array Int Int))
(declare-fun x_36 () (Array Int Int))
(declare-fun x_37 () (Array Int Int))
(declare-fun x_38 () (Array Int Int))
(assert (let ((?v_16 (= x_2 0)) (?v_10 (= x_12 1)) (?v_2 (not (<= x_26 0))) (?v_11 (not (<= x_14 0))) (?v_1 (= x_24 1)) (?v_20 (= x_24 0)) (?v_4 (= x_20 1)) (?v_8 (not (<= x_18 0))) (?v_24 (= x_5 0)) (?v_25 (= x_0 0)) (?v_19 (= x_28 0)) (?v_5 (not (<= x_22 0))) (?v_15 (= x_5 1)) (?v_23 (= x_12 0)) (?v_17 (not (<= x_10 0))) (?v_0 (= x_28 1)) (?v_7 (= x_16 1)) (?v_22 (= x_16 0)) (?v_21 (= x_20 0)) (?v_13 (not (<= x_0 0))) (?v_14 (- x_0 1)) (?v_3 (- x_26 1)) (?v_6 (- x_22 1)) (?v_9 (- x_18 1)) (?v_12 (- x_14 1)) (?v_18 (- x_10 1))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_32 2) (>= x_32 0)) (<= x_28 2)) (>= x_28 0)) (<= x_24 2)) (>= x_24 0)) (<= x_20 2)) (>= x_20 0)) (<= x_16 2)) (>= x_16 0)) (<= x_12 2)) (>= x_12 0)) (<= x_5 2)) (>= x_5 0)) (not (< x_0 0))) (not (< x_2 0))) (not (< x_10 0))) (not (< x_13 0))) (not (< x_14 0))) (not (< x_17 0))) (not (< x_18 0))) (not (< x_21 0))) (not (< x_22 0))) (not (< x_25 0))) (not (< x_26 0))) (not (< x_29 0))) (not (< x_30 0))) (not (< x_33 0))) ?v_25) ?v_16) (= x_32 (ite (<= x_33 2) 1 (ite (<= x_33 5) 0 2)))) (= x_28 (ite (<= x_29 2) 1 (ite (<= x_29 5) 0 2)))) (= x_24 (ite (<= x_25 2) 1 (ite (<= x_25 5) 0 2)))) (= x_20 (ite (<= x_21 2) 1 (ite (<= x_21 5) 0 2)))) (= x_16 (ite (<= x_17 2) 1 (ite (<= x_17 5) 0 2)))) (= x_12 (ite (<= x_13 2) 1 (ite (<= x_13 5) 0 2)))) (= (select x_3 0) (ite ?v_13 (select x_1 ?v_14) x_4))) (= x_5 (ite (<= x_2 2) 1 (ite (<= x_2 5) 0 2)))) (= x_30 (ite ?v_0 (+ x_26 1) (ite (and ?v_19 ?v_2) ?v_3 x_26)))) (= x_31 (ite ?v_0 (store x_27 x_26 (ite (= x_29 0) x_6 (ite (= x_29 1) x_7 (ite (= x_29 2) x_8 x_9)))) x_27))) (= x_33 (+ x_29 1))) (= x_26 (ite ?v_1 (+ x_22 1) (ite (and ?v_20 ?v_5) ?v_6 x_22)))) (= x_27 (ite ?v_1 (store x_23 x_22 (ite (= x_25 0) x_6 (ite (= x_25 1) x_7 (ite (= x_25 2) x_8 x_9)))) x_23))) (= x_29 (+ x_25 1))) (= x_38 (store x_37 x_29 (ite ?v_2 (select x_27 ?v_3) x_4)))) (= x_22 (ite ?v_4 (+ x_18 1) (ite (and ?v_21 ?v_8) ?v_9 x_18)))) (= x_23 (ite ?v_4 (store x_19 x_18 (ite (= x_21 0) x_6 (ite (= x_21 1) x_7 (ite (= x_21 2) x_8 x_9)))) x_19))) (= x_25 (+ x_21 1))) (= x_37 (store x_36 x_25 (ite ?v_5 (select x_23 ?v_6) x_4)))) (= x_18 (ite ?v_7 (+ x_14 1) (ite (and ?v_22 ?v_11) ?v_12 x_14)))) (= x_19 (ite ?v_7 (store x_15 x_14 (ite (= x_17 0) x_6 (ite (= x_17 1) x_7 (ite (= x_17 2) x_8 x_9)))) x_15))) (= x_21 (+ x_17 1))) (= x_36 (store x_35 x_21 (ite ?v_8 (select x_19 ?v_9) x_4)))) (= x_14 (ite ?v_10 (+ x_10 1) (ite (and ?v_23 ?v_17) ?v_18 x_10)))) (= x_15 (ite ?v_10 (store x_11 x_10 (ite (= x_13 0) x_6 (ite (= x_13 1) x_7 (ite (= x_13 2) x_8 x_9)))) x_11))) (= x_17 (+ x_13 1))) (= x_35 (store x_34 x_17 (ite ?v_11 (select x_15 ?v_12) x_4)))) (= x_10 (ite ?v_15 (+ x_0 1) (ite (and ?v_24 ?v_13) ?v_14 x_0)))) (= x_11 (ite ?v_15 (store x_1 x_0 (ite ?v_16 x_6 (ite (= x_2 1) x_7 (ite (= x_2 2) x_8 x_9)))) x_1))) (= x_13 (+ x_2 1))) (= x_34 (store x_3 x_13 (ite ?v_17 (select x_11 ?v_18) x_4)))) (or (or (or (or (or (or (and (= x_32 0) (= x_30 0)) (and ?v_19 (= x_26 0))) (and ?v_20 (= x_22 0))) (and ?v_21 (= x_18 0))) (and ?v_22 (= x_14 0))) (and ?v_23 (= x_10 0))) (and ?v_24 ?v_25)))))
(check-sat)
(exit)
(set-logic QF_ALIA)
(set-info :source |
Benchmarks from Leonardo de Moura <demoura@csl.sri.com>
This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun x_0 () Int)
(declare-fun x_1 () (Array Int Int))
(declare-fun x_2 () Int)
(declare-fun x_3 () (Array Int Int))
(declare-fun x_4 () Int)
(declare-fun x_5 () Int)
(declare-fun x_6 () Int)
(declare-fun x_7 () Int)
(declare-fun x_8 () Int)
(declare-fun x_9 () Int)
(declare-fun x_10 () Int)
(declare-fun x_11 () (Array Int Int))
(declare-fun x_12 () Int)
(declare-fun x_13 () Int)
(declare-fun x_14 () Int)
(declare-fun x_15 () (Array Int Int))
(declare-fun x_16 () Int)
(declare-fun x_17 () Int)
(declare-fun x_18 () Int)
(declare-fun x_19 () (Array Int Int))
(declare-fun x_20 () Int)
(declare-fun x_21 () Int)
(declare-fun x_22 () Int)
(declare-fun x_23 () (Array Int Int))
(declare-fun x_24 () Int)
(declare-fun x_25 () Int)
(declare-fun x_26 () Int)
(declare-fun x_27 () (Array Int Int))
(declare-fun x_28 () Int)
(declare-fun x_29 () Int)
(declare-fun x_30 () Int)
(declare-fun x_31 () (Array Int Int))
(declare-fun x_32 () Int)
(declare-fun x_33 () Int)
(declare-fun x_34 () (Array Int Int))
(declare-fun x_35 () (Array Int Int))
(declare-fun x_36 () (Array Int Int))
(declare-fun x_37 () (Array Int Int))
(declare-fun x_38 () (Array Int Int))
(assert (let ((?v_8 (not (<= x_18 0))) (?v_4 (= x_20 1)) (?v_16 (= x_2 0)) (?v_2 (not (<= x_26 0))) (?v_17 (not (<= x_10 0))) (?v_10 (= x_12 1)) (?v_0 (= x_28 1)) (?v_7 (= x_16 1)) (?v_11 (not (<= x_14 0))) (?v_5 (not (<= x_22 0))) (?v_1 (= x_24 1)) (?v_15 (= x_5 1)) (?v_19 (store x_38 x_33 (ite (not (<= x_30 0)) (select x_31 (- x_30 1)) x_4))) (?v_13 (not (<= x_0 0))) (?v_14 (- x_0 1)) (?v_3 (- x_26 1)) (?v_6 (- x_22 1)) (?v_9 (- x_18 1)) (?v_12 (- x_14 1)) (?v_18 (- x_10 1))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_32 2) (>= x_32 0)) (<= x_28 2)) (>= x_28 0)) (<= x_24 2)) (>= x_24 0)) (<= x_20 2)) (>= x_20 0)) (<= x_16 2)) (>= x_16 0)) (<= x_12 2)) (>= x_12 0)) (<= x_5 2)) (>= x_5 0)) (not (< x_0 0))) (not (< x_2 0))) (not (< x_10 0))) (not (< x_13 0))) (not (< x_14 0))) (not (< x_17 0))) (not (< x_18 0))) (not (< x_21 0))) (not (< x_22 0))) (not (< x_25 0))) (not (< x_26 0))) (not (< x_29 0))) (not (< x_30 0))) (not (< x_33 0))) (= x_0 0)) ?v_16) (= x_32 (ite (<= x_33 2) 1 (ite (<= x_33 5) 0 2)))) (= x_28 (ite (<= x_29 2) 1 (ite (<= x_29 5) 0 2)))) (= x_24 (ite (<= x_25 2) 1 (ite (<= x_25 5) 0 2)))) (= x_20 (ite (<= x_21 2) 1 (ite (<= x_21 5) 0 2)))) (= x_16 (ite (<= x_17 2) 1 (ite (<= x_17 5) 0 2)))) (= x_12 (ite (<= x_13 2) 1 (ite (<= x_13 5) 0 2)))) (= (select x_3 0) (ite ?v_13 (select x_1 ?v_14) x_4))) (= x_5 (ite (<= x_2 2) 1 (ite (<= x_2 5) 0 2)))) (= x_30 (ite ?v_0 (+ x_26 1) (ite (and (= x_28 0) ?v_2) ?v_3 x_26)))) (= x_31 (ite ?v_0 (store x_27 x_26 (ite (= x_29 0) x_6 (ite (= x_29 1) x_7 (ite (= x_29 2) x_8 x_9)))) x_27))) (= x_33 (+ x_29 1))) (= x_26 (ite ?v_1 (+ x_22 1) (ite (and (= x_24 0) ?v_5) ?v_6 x_22)))) (= x_27 (ite ?v_1 (store x_23 x_22 (ite (= x_25 0) x_6 (ite (= x_25 1) x_7 (ite (= x_25 2) x_8 x_9)))) x_23))) (= x_29 (+ x_25 1))) (= x_38 (store x_37 x_29 (ite ?v_2 (select x_27 ?v_3) x_4)))) (= x_22 (ite ?v_4 (+ x_18 1) (ite (and (= x_20 0) ?v_8) ?v_9 x_18)))) (= x_23 (ite ?v_4 (store x_19 x_18 (ite (= x_21 0) x_6 (ite (= x_21 1) x_7 (ite (= x_21 2) x_8 x_9)))) x_19))) (= x_25 (+ x_21 1))) (= x_37 (store x_36 x_25 (ite ?v_5 (select x_23 ?v_6) x_4)))) (= x_18 (ite ?v_7 (+ x_14 1) (ite (and (= x_16 0) ?v_11) ?v_12 x_14)))) (= x_19 (ite ?v_7 (store x_15 x_14 (ite (= x_17 0) x_6 (ite (= x_17 1) x_7 (ite (= x_17 2) x_8 x_9)))) x_15))) (= x_21 (+ x_17 1))) (= x_36 (store x_35 x_21 (ite ?v_8 (select x_19 ?v_9) x_4)))) (= x_14 (ite ?v_10 (+ x_10 1) (ite (and (= x_12 0) ?v_17) ?v_18 x_10)))) (= x_15 (ite ?v_10 (store x_11 x_10 (ite (= x_13 0) x_6 (ite (= x_13 1) x_7 (ite (= x_13 2) x_8 x_9)))) x_11))) (= x_17 (+ x_13 1))) (= x_35 (store x_34 x_17 (ite ?v_11 (select x_15 ?v_12) x_4)))) (= x_10 (ite ?v_15 (+ x_0 1) (ite (and (= x_5 0) ?v_13) ?v_14 x_0)))) (= x_11 (ite ?v_15 (store x_1 x_0 (ite ?v_16 x_6 (ite (= x_2 1) x_7 (ite (= x_2 2) x_8 x_9)))) x_1))) (= x_13 (+ x_2 1))) (= x_34 (store x_3 x_13 (ite ?v_17 (select x_11 ?v_18) x_4)))) (or (or (or (or (or (or (and (not (< x_33 6)) (or (or (not (= (select ?v_19 3) x_6)) (not (= (select ?v_19 4) x_7))) (not (= (select ?v_19 5) x_8)))) (and (not (< x_29 6)) (or (or (not (= (select x_38 3) x_6)) (not (= (select x_38 4) x_7))) (not (= (select x_38 5) x_8))))) (and (not (< x_25 6)) (or (or (not (= (select x_37 3) x_6)) (not (= (select x_37 4) x_7))) (not (= (select x_37 5) x_8))))) (and (not (< x_21 6)) (or (or (not (= (select x_36 3) x_6)) (not (= (select x_36 4) x_7))) (not (= (select x_36 5) x_8))))) (and (not (< x_17 6)) (or (or (not (= (select x_35 3) x_6)) (not (= (select x_35 4) x_7))) (not (= (select x_35 5) x_8))))) (and (not (< x_13 6)) (or (or (not (= (select x_34 3) x_6)) (not (= (select x_34 4) x_7))) (not (= (select x_34 5) x_8))))) (and (not (< x_2 6)) (or (or (not (= (select x_3 3) x_6)) (not (= (select x_3 4) x_7))) (not (= (select x_3 5) x_8))))))))
(check-sat)
(exit)
(set-logic QF_ALIA)
(set-info :source |
Benchmarks from Leonardo de Moura <demoura@csl.sri.com>
This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Int)
(declare-fun x_1 () (Array Int Int))
(declare-fun x_2 () Int)
(declare-fun x_3 () (Array Int Int))
(declare-fun x_4 () Int)
(declare-fun x_5 () Int)
(declare-fun x_6 () Int)
(declare-fun x_7 () Int)
(declare-fun x_8 () Int)
(declare-fun x_9 () Int)
(declare-fun x_10 () Int)
(declare-fun x_11 () (Array Int Int))
(declare-fun x_12 () Int)
(declare-fun x_13 () Int)
(declare-fun x_14 () Int)
(declare-fun x_15 () (Array Int Int))
(declare-fun x_16 () Int)
(declare-fun x_17 () Int)
(declare-fun x_18 () Int)
(declare-fun x_19 () (Array Int Int))
(declare-fun x_20 () Int)
(declare-fun x_21 () Int)
(declare-fun x_22 () Int)
(declare-fun x_23 () (Array Int Int))
(declare-fun x_24 () Int)
(declare-fun x_25 () Int)
(declare-fun x_26 () Int)
(declare-fun x_27 () (Array Int Int))
(declare-fun x_28 () Int)
(declare-fun x_29 () Int)
(declare-fun x_30 () Int)
(declare-fun x_31 () (Array Int Int))
(declare-fun x_32 () Int)
(declare-fun x_33 () Int)
(declare-fun x_34 () (Array Int Int))
(declare-fun x_35 () (Array Int Int))
(declare-fun x_36 () (Array Int Int))
(declare-fun x_37 () (Array Int Int))
(declare-fun x_38 () (Array Int Int))
(assert (let ((?v_10 (= x_12 1)) (?v_5 (not (<= x_22 0))) (?v_7 (= x_16 1)) (?v_11 (not (<= x_14 0))) (?v_17 (not (<= x_10 0))) (?v_8 (not (<= x_18 0))) (?v_16 (= x_2 0)) (?v_1 (= x_24 1)) (?v_2 (not (<= x_26 0))) (?v_15 (= x_5 1)) (?v_0 (= x_28 1)) (?v_4 (= x_20 1)) (?v_19 (store x_38 x_33 (ite (not (<= x_30 0)) (select x_31 (- x_30 1)) x_4))) (?v_13 (not (<= x_0 0))) (?v_14 (- x_0 1)) (?v_3 (- x_26 1)) (?v_6 (- x_22 1)) (?v_9 (- x_18 1)) (?v_12 (- x_14 1)) (?v_18 (- x_10 1))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_32 2) (>= x_32 0)) (<= x_28 2)) (>= x_28 0)) (<= x_24 2)) (>= x_24 0)) (<= x_20 2)) (>= x_20 0)) (<= x_16 2)) (>= x_16 0)) (<= x_12 2)) (>= x_12 0)) (<= x_5 2)) (>= x_5 0)) (not (< x_0 0))) (not (< x_2 0))) (not (< x_10 0))) (not (< x_13 0))) (not (< x_14 0))) (not (< x_17 0))) (not (< x_18 0))) (not (< x_21 0))) (not (< x_22 0))) (not (< x_25 0))) (not (< x_26 0))) (not (< x_29 0))) (not (< x_30 0))) (not (< x_33 0))) (= x_0 0)) ?v_16) (= x_32 (ite (<= x_33 2) 1 (ite (<= x_33 5) 0 2)))) (= x_28 (ite (<= x_29 2) 1 (ite (<= x_29 5) 0 2)))) (= x_24 (ite (<= x_25 2) 1 (ite (<= x_25 5) 0 2)))) (= x_20 (ite (<= x_21 2) 1 (ite (<= x_21 5) 0 2)))) (= x_16 (ite (<= x_17 2) 1 (ite (<= x_17 5) 0 2)))) (= x_12 (ite (<= x_13 2) 1 (ite (<= x_13 5) 0 2)))) (= (select x_3 0) (ite ?v_13 (select x_1 ?v_14) x_4))) (= x_5 (ite (<= x_2 2) 1 (ite (<= x_2 5) 0 2)))) (= x_30 (ite ?v_0 (+ x_26 1) (ite (and (= x_28 0) ?v_2) ?v_3 x_26)))) (= x_31 (ite ?v_0 (store x_27 x_26 (ite (= x_29 0) x_6 (ite (= x_29 1) x_7 (ite (= x_29 2) x_8 x_9)))) x_27))) (= x_33 (+ x_29 1))) (= x_26 (ite ?v_1 (+ x_22 1) (ite (and (= x_24 0) ?v_5) ?v_6 x_22)))) (= x_27 (ite ?v_1 (store x_23 x_22 (ite (= x_25 0) x_6 (ite (= x_25 1) x_7 (ite (= x_25 2) x_8 x_9)))) x_23))) (= x_29 (+ x_25 1))) (= x_38 (store x_37 x_29 (ite ?v_2 (select x_27 ?v_3) x_4)))) (= x_22 (ite ?v_4 (+ x_18 1) (ite (and (= x_20 0) ?v_8) ?v_9 x_18)))) (= x_23 (ite ?v_4 (store x_19 x_18 (ite (= x_21 0) x_6 (ite (= x_21 1) x_7 (ite (= x_21 2) x_8 x_9)))) x_19))) (= x_25 (+ x_21 1))) (= x_37 (store x_36 x_25 (ite ?v_5 (select x_23 ?v_6) x_4)))) (= x_18 (ite ?v_7 (+ x_14 1) (ite (and (= x_16 0) ?v_11) ?v_12 x_14)))) (= x_19 (ite ?v_7 (store x_15 x_14 (ite (= x_17 0) x_6 (ite (= x_17 1) x_7 (ite (= x_17 2) x_8 x_9)))) x_15))) (= x_21 (+ x_17 1))) (= x_36 (store x_35 x_21 (ite ?v_8 (select x_19 ?v_9) x_4)))) (= x_14 (ite ?v_10 (+ x_10 1) (ite (and (= x_12 0) ?v_17) ?v_18 x_10)))) (= x_15 (ite ?v_10 (store x_11 x_10 (ite (= x_13 0) x_6 (ite (= x_13 1) x_7 (ite (= x_13 2) x_8 x_9)))) x_11))) (= x_17 (+ x_13 1))) (= x_35 (store x_34 x_17 (ite ?v_11 (select x_15 ?v_12) x_4)))) (= x_10 (ite ?v_15 (+ x_0 1) (ite (and (= x_5 0) ?v_13) ?v_14 x_0)))) (= x_11 (ite ?v_15 (store x_1 x_0 (ite ?v_16 x_6 (ite (= x_2 1) x_7 (ite (= x_2 2) x_8 x_9)))) x_1))) (= x_13 (+ x_2 1))) (= x_34 (store x_3 x_13 (ite ?v_17 (select x_11 ?v_18) x_4)))) (or (or (or (or (or (or (and (not (< x_33 6)) (or (or (not (= (select ?v_19 3) x_8)) (not (= (select ?v_19 4) x_7))) (not (= (select ?v_19 5) x_6)))) (and (not (< x_29 6)) (or (or (not (= (select x_38 3) x_8)) (not (= (select x_38 4) x_7))) (not (= (select x_38 5) x_6))))) (and (not (< x_25 6)) (or (or (not (= (select x_37 3) x_8)) (not (= (select x_37 4) x_7))) (not (= (select x_37 5) x_6))))) (and (not (< x_21 6)) (or (or (not (= (select x_36 3) x_8)) (not (= (select x_36 4) x_7))) (not (= (select x_36 5) x_6))))) (and (not (< x_17 6)) (or (or (not (= (select x_35 3) x_8)) (not (= (select x_35 4) x_7))) (not (= (select x_35 5) x_6))))) (and (not (< x_13 6)) (or (or (not (= (select x_34 3) x_8)) (not (= (select x_34 4) x_7))) (not (= (select x_34 5) x_6))))) (and (not (< x_2 6)) (or (or (not (= (select x_3 3) x_8)) (not (= (select x_3 4) x_7))) (not (= (select x_3 5) x_6))))))))
(check-sat)
(exit)
no description
\ No newline at end of file
This diff is collapsed.
(set-logic QF_ALIA)
(set-info :source |
Benchmarks from Leonardo de Moura <demoura@csl.sri.com>
This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun x_0 () Int)
(declare-fun x_1 () Int)
(declare-fun x_2 () Int)
(declare-fun x_3 () Int)
(declare-fun x_4 () (Array Int Int))
(declare-fun x_5 () Int)
(declare-fun x_6 () Int)
(declare-fun x_7 () Int)
(declare-fun x_8 () Int)
(declare-fun x_9 () Int)
(declare-fun x_10 () (Array Int Int))
(declare-fun x_11 () (Array Int Int))
(declare-fun x_12 () Int)
(declare-fun x_13 () Int)
(declare-fun x_14 () Int)
(declare-fun x_15 () Int)
(declare-fun x_16 () (Array Int Int))
(declare-fun x_17 () Int)
(declare-fun x_18 () Int)
(declare-fun x_19 () Int)
(declare-fun x_20 () Int)
(declare-fun x_21 () Int)
(declare-fun x_22 () Int)
(declare-fun x_23 () Int)
(declare-fun x_24 () (Array Int Int))
(declare-fun x_25 () Int)
(declare-fun x_26 () Int)
(declare-fun x_27 () Int)
(declare-fun x_28 () (Array Int Int))
(declare-fun x_29 () Int)
(declare-fun x_30 () Int)
(declare-fun x_31 () Int)
(declare-fun x_32 () Int)
(declare-fun x_33 () Int)
(declare-fun x_34 () Int)
(declare-fun x_35 () (Array Int Int))
(declare-fun x_36 () Int)
(declare-fun x_37 () Int)
(declare-fun x_38 () Int)
(declare-fun x_39 () (Array Int Int))
(declare-fun x_40 () Int)
(declare-fun x_41 () Int)
(declare-fun x_42 () Int)
(declare-fun x_43 () Int)
(declare-fun x_44 () Int)
(declare-fun x_45 () Int)
(declare-fun x_46 () (Array Int Int))
(declare-fun x_47 () Int)
(declare-fun x_48 () Int)
(declare-fun x_49 () Int)
(declare-fun x_50 () (Array Int Int))
(declare-fun x_51 () Int)
(declare-fun x_52 () Int)
(declare-fun x_53 () Int)
(declare-fun x_54 () Int)
(declare-fun x_55 () Int)
(declare-fun x_56 () Int)
(declare-fun x_57 () (Array Int Int))
(declare-fun x_58 () Int)
(declare-fun x_59 () Int)
(declare-fun x_60 () Int)
(declare-fun x_61 () (Array Int Int))
(declare-fun x_62 () Int)
(declare-fun x_63 () Int)
(declare-fun x_64 () Int)
(declare-fun x_65 () Int)
(declare-fun x_66 () Int)
(declare-fun x_67 () Int)
(declare-fun x_68 () Int)
(assert (let ((?v_35 (= x_6 (+ x_0 1))) (?v_41 (= x_9 x_2)) (?v_37 (= x_10 x_11)) (?v_36 (= x_12 x_13)) (?v_38 (= x_14 x_1)) (?v_39 (= x_15 x_3)) (?v_42 (= x_16 x_4)) (?v_40 (= x_17 x_18)) (?v_26 (= x_21 (+ x_6 1))) (?v_32 (= x_23 x_9)) (?v_28 (= x_24 x_10)) (?v_27 (= x_25 x_12)) (?v_29 (= x_26 x_14)) (?v_30 (= x_27 x_15)) (?v_33 (= x_28 x_16)) (?v_31 (= x_29 x_17)) (?v_18 (= x_32 (+ x_21 1))) (?v_24 (= x_34 x_23)) (?v_20 (= x_35 x_24)) (?v_19 (= x_36 x_25)) (?v_21 (= x_37 x_26)) (?v_22 (= x_38 x_27)) (?v_25 (= x_39 x_28)) (?v_23 (= x_40 x_29)) (?v_9 (= x_43 (+ x_32 1))) (?v_16 (= x_45 x_34)) (?v_12 (= x_46 x_35)) (?v_10 (= x_47 x_36)) (?v_13 (= x_48 x_37)) (?v_14 (= x_49 x_38)) (?v_17 (= x_50 x_39)) (?v_15 (= x_51 x_40)) (?v_1 (= x_54 (+ x_43 1))) (?v_7 (= x_56 x_45)) (?v_3 (= x_57 x_46)) (?v_2 (= x_58 x_47)) (?v_4 (= x_59 x_48)) (?v_5 (= x_60 x_49)) (?v_8 (= x_61 x_50)) (?v_6 (= x_62 x_51)) (?v_0 (+ x_7 2)) (?v_11 (+ x_7 1)) (?v_34 (= x_2 (- 1))) (?v_43 (= x_45 (- 1))) (?v_44 (= x_34 (- 1))) (?v_45 (= x_23 (- 1))) (?v_46 (= x_9 (- 1)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (<= x_7 0)) (= x_0 0)) (= x_1 0)) ?v_34) (= x_3 0)) (= x_64 (select x_4 x_2))) (= x_5 x_64)) (= x_8 ?v_0)) (= x_65 (select x_16 x_9))) (= x_20 x_65)) (= x_22 ?v_0)) (= x_66 (select x_28 x_23))) (= x_31 x_66)) (= x_33 ?v_0)) (= x_67 (select x_39 x_34))) (= x_42 x_67)) (= x_44 ?v_0)) (= x_68 (select x_50 x_45))) (= x_53 x_68)) (= x_55 ?v_0)) (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_63 0) (< x_43 x_7)) ?v_1) (= x_60 (+ x_49 1))) (= x_56 x_48)) (= x_59 (+ x_48 1))) (= x_57 (store x_46 x_48 x_43))) ?v_2) (= x_61 (store x_50 x_48 x_45))) ?v_6) (and (and (and (and (and (and (and (and (and (and (= x_63 1) (= x_43 x_7)) (not ?v_43)) (= x_62 x_45)) (= x_56 x_53)) ?v_1) ?v_3) ?v_2) ?v_4) ?v_5) ?v_8)) (and (and (and (and (and (and (and (and (and (= x_63 2) (= x_43 ?v_11)) ?v_1) ?v_7) ?v_3) ?v_2) ?v_4) ?v_5) (= x_61 (store x_50 x_51 x_53))) ?v_6)) (and (and (and (and (and (and (and (and (and (= x_63 3) (= x_43 x_55)) ?v_1) ?v_7) ?v_3) ?v_2) ?v_4) ?v_5) (= x_61 (store x_50 x_45 x_51))) ?v_6)) (and (and (and (and (and (and (and (and (and (= x_63 4) (not (<= x_43 x_55))) ?v_7) ?v_3) ?v_2) ?v_4) ?v_5) ?v_8) ?v_6) (= x_54 x_43)))) (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_52 0) (< x_32 x_7)) ?v_9) (= x_49 (+ x_38 1))) (= x_45 x_37)) (= x_48 (+ x_37 1))) (= x_46 (store x_35 x_37 x_32))) ?v_10) (= x_50 (store x_39 x_37 x_34))) ?v_15) (and (and (and (and (and (and (and (and (and (and (= x_52 1) (= x_32 x_7)) (not ?v_44)) (= x_51 x_34)) (= x_45 x_42)) ?v_9) ?v_12) ?v_10) ?v_13) ?v_14) ?v_17)) (and (and (and (and (and (and (and (and (and (= x_52 2) (= x_32 ?v_11)) ?v_9) ?v_16) ?v_12) ?v_10) ?v_13) ?v_14) (= x_50 (store x_39 x_40 x_42))) ?v_15)) (and (and (and (and (and (and (and (and (and (= x_52 3) (= x_32 x_44)) ?v_9) ?v_16) ?v_12) ?v_10) ?v_13) ?v_14) (= x_50 (store x_39 x_34 x_40))) ?v_15)) (and (and (and (and (and (and (and (and (and (= x_52 4) (not (<= x_32 x_44))) ?v_16) ?v_12) ?v_10) ?v_13) ?v_14) ?v_17) ?v_15) (= x_43 x_32)))) (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_41 0) (< x_21 x_7)) ?v_18) (= x_38 (+ x_27 1))) (= x_34 x_26)) (= x_37 (+ x_26 1))) (= x_35 (store x_24 x_26 x_21))) ?v_19) (= x_39 (store x_28 x_26 x_23))) ?v_23) (and (and (and (and (and (and (and (and (and (and (= x_41 1) (= x_21 x_7)) (not ?v_45)) (= x_40 x_23)) (= x_34 x_31)) ?v_18) ?v_20) ?v_19) ?v_21) ?v_22) ?v_25)) (and (and (and (and (and (and (and (and (and (= x_41 2) (= x_21 ?v_11)) ?v_18) ?v_24) ?v_20) ?v_19) ?v_21) ?v_22) (= x_39 (store x_28 x_29 x_31))) ?v_23)) (and (and (and (and (and (and (and (and (and (= x_41 3) (= x_21 x_33)) ?v_18) ?v_24) ?v_20) ?v_19) ?v_21) ?v_22) (= x_39 (store x_28 x_23 x_29))) ?v_23)) (and (and (and (and (and (and (and (and (and (= x_41 4) (not (<= x_21 x_33))) ?v_24) ?v_20) ?v_19) ?v_21) ?v_22) ?v_25) ?v_23) (= x_32 x_21)))) (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_30 0) (< x_6 x_7)) ?v_26) (= x_27 (+ x_15 1))) (= x_23 x_14)) (= x_26 (+ x_14 1))) (= x_24 (store x_10 x_14 x_6))) ?v_27) (= x_28 (store x_16 x_14 x_9))) ?v_31) (and (and (and (and (and (and (and (and (and (and (= x_30 1) (= x_6 x_7)) (not ?v_46)) (= x_29 x_9)) (= x_23 x_20)) ?v_26) ?v_28) ?v_27) ?v_29) ?v_30) ?v_33)) (and (and (and (and (and (and (and (and (and (= x_30 2) (= x_6 ?v_11)) ?v_26) ?v_32) ?v_28) ?v_27) ?v_29) ?v_30) (= x_28 (store x_16 x_17 x_20))) ?v_31)) (and (and (and (and (and (and (and (and (and (= x_30 3) (= x_6 x_22)) ?v_26) ?v_32) ?v_28) ?v_27) ?v_29) ?v_30) (= x_28 (store x_16 x_9 x_17))) ?v_31)) (and (and (and (and (and (and (and (and (and (= x_30 4) (not (<= x_6 x_22))) ?v_32) ?v_28) ?v_27) ?v_29) ?v_30) ?v_33) ?v_31) (= x_21 x_6)))) (or (or (or (or (and (and (and (and (and (and (and (and (and (= x_19 0) (< x_0 x_7)) ?v_35) (= x_15 (+ x_3 1))) (= x_9 x_1)) (= x_14 (+ x_1 1))) (= x_10 (store x_11 x_1 x_0))) ?v_36) (= x_16 (store x_4 x_1 x_2))) ?v_40) (and (and (and (and (and (and (and (and (and (and (= x_19 1) (= x_0 x_7)) (not ?v_34)) (= x_17 x_2)) (= x_9 x_5)) ?v_35) ?v_37) ?v_36) ?v_38) ?v_39) ?v_42)) (and (and (and (and (and (and (and (and (and (= x_19 2) (= x_0 ?v_11)) ?v_35) ?v_41) ?v_37) ?v_36) ?v_38) ?v_39) (= x_16 (store x_4 x_18 x_5))) ?v_40)) (and (and (and (and (and (and (and (and (and (= x_19 3) (= x_0 x_8)) ?v_35) ?v_41) ?v_37) ?v_36) ?v_38) ?v_39) (= x_16 (store x_4 x_2 x_18))) ?v_40)) (and (and (and (and (and (and (and (and (and (= x_19 4) (not (<= x_0 x_8))) ?v_41) ?v_37) ?v_36) ?v_38) ?v_39) ?v_42) ?v_40) (= x_6 x_0)))) (or (or (or (or (or (and (not (<= x_54 0)) (= x_56 (- 1))) (and (not (<= x_43 0)) ?v_43)) (and (not (<= x_32 0)) ?v_44)) (and (not (<= x_21 0)) ?v_45)) (and (not (<= x_6 0)) ?v_46)) (and (not (<= x_0 0)) ?v_34)))))
(check-sat)
(exit)
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment