Commit e0edbfca authored by Alain Mebsout's avatar Alain Mebsout
Browse files

Importing snapshot 2015-06-01

parents
Pipeline #3 skipped
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_7 () Int)
(declare-fun u () Int)
(declare-fun l () Int)
(declare-fun e () Int)
(declare-fun a () (Array Int Int))
(declare-fun ix () Int)
(declare-fun t_1 () Int)
(assert (let ((?v_0 (<= 0 l)) (?v_1 (< u V_7)) (?v_2 (>= V_7 0))) (and (and (and (and ?v_0 (and ?v_1 (forall ((?V_10 Int)) (=> (and (<= 0 ?V_10) (<= ?V_10 (- V_7 1))) (forall ((?V_11 Int)) (=> (and (<= 0 ?V_11) (<= ?V_11 ?V_10)) (<= (select a ?V_11) (select a ?V_10)))))))) ?v_2) (and (= (select a t_1) e) (and (and (<= l t_1) (<= t_1 u)) (and (<= l u) (and (and ?v_0 (and ?v_1 (forall ((?V_8 Int)) (=> (and (<= 0 ?V_8) (<= ?V_8 (- V_7 1))) (forall ((?V_9 Int)) (=> (and (<= 0 ?V_9) (<= ?V_9 ?V_8)) (<= (select a ?V_9) (select a ?V_8)))))))) ?v_2))))) (or (and false (exists ((?V_6 Int)) (and (and (<= l ?V_6) (<= ?V_6 u)) (= (select a ?V_6) e)))) (and true (forall ((?V_5 Int)) (=> (and (<= l ?V_5) (<= ?V_5 u)) (not (= (select a ?V_5) e)))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_6 () Int)
(declare-fun e () Int)
(declare-fun a () (Array Int Int))
(declare-fun ix () Int)
(declare-fun t_1 () Bool)
(assert (let ((?v_0 (>= V_6 0)) (?v_1 (not t_1))) (and (and (and (forall ((?V_12 Int)) (=> (and (<= 0 ?V_12) (<= ?V_12 (- V_6 1))) (forall ((?V_13 Int)) (=> (and (<= 0 ?V_13) (<= ?V_13 ?V_12)) (<= (select a ?V_13) (select a ?V_12)))))) ?v_0) (and (and (or t_1 (forall ((?V_11 Int)) (=> (and (<= 0 ?V_11) (<= ?V_11 (- V_6 1))) (not (= (select a ?V_11) e))))) (or ?v_1 (exists ((?V_10 Int)) (and (and (<= 0 ?V_10) (<= ?V_10 (- V_6 1))) (= (select a ?V_10) e))))) (and (forall ((?V_8 Int)) (=> (and (<= 0 ?V_8) (<= ?V_8 (- V_6 1))) (forall ((?V_9 Int)) (=> (and (<= 0 ?V_9) (<= ?V_9 ?V_8)) (<= (select a ?V_9) (select a ?V_8)))))) ?v_0))) (or (and ?v_1 (exists ((?V_7 Int)) (and (and (<= 0 ?V_7) (<= ?V_7 (- V_6 1))) (= (select a ?V_7) e)))) (and t_1 (forall ((?V_5 Int)) (=> (and (<= 0 ?V_5) (<= ?V_5 (- V_6 1))) (not (= (select a ?V_5) e)))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_6 () Int)
(declare-fun V_5 () Int)
(declare-fun ix () Int)
(declare-fun t () Int)
(declare-fun j () Int)
(declare-fun a_0 () (Array Int Int))
(declare-fun a () (Array Int Int))
(declare-fun i () Int)
(assert (let ((?v_2 (and true (>= V_5 0))) (?v_0 (- i 1))) (let ((?v_1 (= j ?v_0)) (?v_3 (= V_6 V_5))) (and (and ?v_2 (and (<= (select a j) t) (and (>= j 0) (and (and (<= 1 i) (and (< i V_6) (and (<= (- 1) j) (and (<= j ?v_0) (and (forall ((?V_10 Int)) (=> (and (<= 0 ?V_10) (<= ?V_10 ?v_0)) (forall ((?V_11 Int)) (=> (and (<= 0 ?V_11) (<= ?V_11 ?V_10)) (<= (select a ?V_11) (select a ?V_10)))))) (and (or ?v_1 (<= (select a ?v_0) (select a i))) (and (or ?v_1 (forall ((?V_9 Int)) (=> (and (<= (+ j 1) ?V_9) (<= ?V_9 i)) (> (select a ?V_9) t)))) ?v_3))))))) ?v_2)))) (or (> 1 (+ i 1)) (or (exists ((?V_7 Int)) (and (and (<= 0 ?V_7) (<= ?V_7 (- (+ i 1) 1))) (exists ((?V_8 Int)) (let ((?v_4 (store a (+ j 1) t))) (and (and (<= 0 ?V_8) (<= ?V_8 ?V_7)) (> (select ?v_4 ?V_8) (select ?v_4 ?V_7))))))) (not ?v_3)))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_10 () Int)
(declare-fun V_9 () Int)
(declare-fun i () Int)
(declare-fun a () (Array Int Int))
(declare-fun a_0 () (Array Int Int))
(assert (let ((?v_0 (and true (>= V_9 0)))) (and (and ?v_0 (and (<= i 0) (and (and (<= (- 1) i) (and (< i V_10) (and (or (>= i (+ i 1)) (forall ((?V_13 Int)) (=> (and (<= 0 ?V_13) (<= ?V_13 i)) (forall ((?V_14 Int)) (=> (and (<= (+ i 1) ?V_14) (<= ?V_14 (- V_10 1))) (<= (select a ?V_13) (select a ?V_14))))))) (and (forall ((?V_11 Int)) (=> (and (<= i ?V_11) (<= ?V_11 (- V_10 1))) (forall ((?V_12 Int)) (=> (and (<= i ?V_12) (<= ?V_12 ?V_11)) (<= (select a ?V_12) (select a ?V_11)))))) (= V_10 V_9))))) ?v_0))) (exists ((?V_7 Int)) (and (and (<= 0 ?V_7) (<= ?V_7 (- V_9 1))) (exists ((?V_8 Int)) (and (and (<= 0 ?V_8) (<= ?V_8 ?V_7)) (> (select a ?V_8) (select a ?V_7)))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_10 () Int)
(declare-fun V_9 () Int)
(declare-fun arr () (Array Int Int))
(declare-fun t_1 () (Array Int Int))
(assert (let ((?v_0 (and true (>= V_10 0)))) (and (and ?v_0 (and (and (forall ((?V_13 Int)) (=> (and (<= 0 ?V_13) (<= ?V_13 (- V_10 1))) (forall ((?V_14 Int)) (=> (and (<= 0 ?V_14) (<= ?V_14 ?V_13)) (<= (select t_1 ?V_14) (select t_1 ?V_13)))))) (and (= V_9 V_10) (and (forall ((?V_12 Int)) (=> (and (<= 0 ?V_12) (<= ?V_12 (- 0 1))) (= (select t_1 ?V_12) (select arr ?V_12)))) (forall ((?V_11 Int)) (let ((?v_1 (- V_10 1))) (=> (and (<= (+ ?v_1 1) ?V_11) (<= ?V_11 ?v_1)) (= (select t_1 ?V_11) (select arr ?V_11)))))))) ?v_0)) (exists ((?V_7 Int)) (and (and (<= 0 ?V_7) (<= ?V_7 (- V_9 1))) (exists ((?V_8 Int)) (and (and (<= 0 ?V_8) (<= ?V_8 ?V_7)) (> (select t_1 ?V_8) (select t_1 ?V_7)))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_26 () Int)
(declare-fun V_23 () Int)
(declare-fun V_22 () Int)
(declare-fun j () Int)
(declare-fun i () Int)
(declare-fun u_0 () Int)
(declare-fun m_0 () Int)
(declare-fun m () Int)
(declare-fun l_0 () Int)
(declare-fun arr_0 () (Array Int Int))
(declare-fun u () Int)
(declare-fun arr () (Array Int Int))
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun buf () (Array Int Int))
(assert (let ((?v_3 (<= 0 l_0)) (?v_4 (<= l_0 m_0)) (?v_5 (< m_0 u_0)) (?v_6 (< u_0 V_22)) (?v_7 (>= V_22 0)) (?v_0 (+ m 1)) (?v_1 (= k 0)) (?v_2 (select buf (- k 1))) (?v_8 (= V_26 (+ (- u l) 1))) (?v_9 (= V_23 V_22)) (?v_10 (= l l_0)) (?v_11 (= m m_0)) (?v_12 (= u u_0))) (and (and (and (and ?v_3 (and ?v_4 (and ?v_5 (and ?v_6 (and (forall ((?V_44 Int)) (=> (and (<= l_0 ?V_44) (<= ?V_44 m_0)) (forall ((?V_45 Int)) (=> (and (<= l_0 ?V_45) (<= ?V_45 ?V_44)) (<= (select arr_0 ?V_45) (select arr_0 ?V_44)))))) (forall ((?V_42 Int)) (=> (and (<= (+ m_0 1) ?V_42) (<= ?V_42 u_0)) (forall ((?V_43 Int)) (=> (and (<= (+ m_0 1) ?V_43) (<= ?V_43 ?V_42)) (<= (select arr_0 ?V_43) (select arr_0 ?V_42))))))))))) ?v_7) (and (>= k V_26) (and (and (<= l i) (and (<= i ?v_0) (and (<= ?v_0 j) (and (<= j (+ u 1)) (and (= k (+ (- i l) (- j ?v_0))) (and (forall ((?V_40 Int)) (=> (and (<= l ?V_40) (<= ?V_40 m)) (forall ((?V_41 Int)) (=> (and (<= l ?V_41) (<= ?V_41 ?V_40)) (<= (select arr ?V_41) (select arr ?V_40)))))) (and (forall ((?V_38 Int)) (=> (and (<= ?v_0 ?V_38) (<= ?V_38 u)) (forall ((?V_39 Int)) (=> (and (<= ?v_0 ?V_39) (<= ?V_39 ?V_38)) (<= (select arr ?V_39) (select arr ?V_38)))))) (and (or (= k V_26) (or (<= i m) (<= j u))) (and (or ?v_1 (or (> i m) (<= ?v_2 (select arr i)))) (and (or ?v_1 (or (> j u) (<= ?v_2 (select arr j)))) (and (forall ((?V_36 Int)) (=> (and (<= 0 ?V_36) (<= ?V_36 (- k 1))) (forall ((?V_37 Int)) (=> (and (<= 0 ?V_37) (<= ?V_37 ?V_36)) (<= (select buf ?V_37) (select buf ?V_36)))))) (and ?v_8 (and (forall ((?V_35 Int)) (=> (and (<= 0 ?V_35) (<= ?V_35 (- V_23 1))) (= (select arr ?V_35) (select arr_0 ?V_35)))) (and ?v_9 (and ?v_10 (and ?v_11 ?v_12)))))))))))))))) (and (and ?v_3 (and ?v_4 (and ?v_5 (and ?v_6 (and (forall ((?V_33 Int)) (=> (and (<= l_0 ?V_33) (<= ?V_33 m_0)) (forall ((?V_34 Int)) (=> (and (<= l_0 ?V_34) (<= ?V_34 ?V_33)) (<= (select arr_0 ?V_34) (select arr_0 ?V_33)))))) (forall ((?V_31 Int)) (=> (and (<= (+ m_0 1) ?V_31) (<= ?V_31 u_0)) (forall ((?V_32 Int)) (=> (and (<= (+ m_0 1) ?V_32) (<= ?V_32 ?V_31)) (<= (select arr_0 ?V_32) (select arr_0 ?V_31))))))))))) ?v_7)))) (or (exists ((?V_29 Int)) (and (and (<= 0 ?V_29) (<= ?V_29 (- V_26 1))) (exists ((?V_30 Int)) (and (and (<= 0 ?V_30) (<= ?V_30 ?V_29)) (> (select buf ?V_30) (select buf ?V_29)))))) (or (exists ((?V_27 Int)) (and (and (<= l ?V_27) (<= ?V_27 (- (+ l 0) 1))) (exists ((?V_28 Int)) (and (and (<= l ?V_28) (<= ?V_28 ?V_27)) (> (select arr ?V_28) (select arr ?V_27)))))) (or (and (not (= 0 0)) (and (not (= 0 V_26)) (> (select arr (- (+ l 0) 1)) (select buf 0)))) (or (> 0 0) (or (> 0 V_26) (or (not ?v_8) (or (exists ((?V_25 Int)) (and (and (<= 0 ?V_25) (<= ?V_25 (- l 1))) (not (= (select arr ?V_25) (select arr_0 ?V_25))))) (or (exists ((?V_24 Int)) (and (and (<= (+ u 1) ?V_24) (<= ?V_24 (- V_23 1))) (not (= (select arr ?V_24) (select arr_0 ?V_24))))) (or (not ?v_9) (or (not ?v_10) (or (not ?v_11) (not ?v_12)))))))))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_7 () Int)
(declare-fun l () Int)
(declare-fun u () Int)
(declare-fun e () Int)
(declare-fun a () (Array Int Int))
(declare-fun ix () Int)
(declare-fun t_2 () Bool)
(declare-fun t_1 () Int)
(assert (let ((?v_1 (<= 0 l)) (?v_2 (< u V_7)) (?v_3 (>= V_7 0)) (?v_4 (not t_2)) (?v_0 (select a t_1))) (and (and (and (and ?v_1 (and ?v_2 (forall ((?V_12 Int)) (=> (and (<= 0 ?V_12) (<= ?V_12 (- V_7 1))) (forall ((?V_13 Int)) (=> (and (<= 0 ?V_13) (<= ?V_13 ?V_12)) (<= (select a ?V_13) (select a ?V_12)))))))) ?v_3) (and (and (or t_2 (forall ((?V_11 Int)) (=> (and (<= (+ t_1 1) ?V_11) (<= ?V_11 u)) (not (= (select a ?V_11) e))))) (or ?v_4 (exists ((?V_10 Int)) (and (and (<= (+ t_1 1) ?V_10) (<= ?V_10 u)) (= (select a ?V_10) e))))) (and (< ?v_0 e) (and (not (= ?v_0 e)) (and (and (<= l t_1) (<= t_1 u)) (and (<= l u) (and (and ?v_1 (and ?v_2 (forall ((?V_8 Int)) (=> (and (<= 0 ?V_8) (<= ?V_8 (- V_7 1))) (forall ((?V_9 Int)) (=> (and (<= 0 ?V_9) (<= ?V_9 ?V_8)) (<= (select a ?V_9) (select a ?V_8)))))))) ?v_3))))))) (or (and ?v_4 (exists ((?V_6 Int)) (and (and (<= l ?V_6) (<= ?V_6 u)) (= (select a ?V_6) e)))) (and t_2 (forall ((?V_5 Int)) (=> (and (<= l ?V_5) (<= ?V_5 u)) (not (= (select a ?V_5) e)))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_25 () Int)
(declare-fun V_22 () Int)
(declare-fun V_21 () Int)
(declare-fun u_0 () Int)
(declare-fun m_0 () Int)
(declare-fun m () Int)
(declare-fun l_0 () Int)
(declare-fun arr_0 () (Array Int Int))
(declare-fun u () Int)
(declare-fun arr () (Array Int Int))
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun buf () (Array Int Int))
(assert (let ((?v_0 (<= 0 l_0)) (?v_1 (<= l_0 m_0)) (?v_2 (< m_0 u_0)) (?v_3 (< u_0 V_21)) (?v_4 (>= V_21 0)) (?v_6 (+ l k)) (?v_7 (select buf k)) (?v_8 (= V_25 (+ (- u l) 1))) (?v_9 (= V_22 V_21)) (?v_10 (= l l_0)) (?v_11 (= m m_0)) (?v_12 (= u u_0)) (?v_5 (+ k 1))) (and (and (and (and ?v_0 (and ?v_1 (and ?v_2 (and ?v_3 (and (forall ((?V_42 Int)) (=> (and (<= l_0 ?V_42) (<= ?V_42 m_0)) (forall ((?V_43 Int)) (=> (and (<= l_0 ?V_43) (<= ?V_43 ?V_42)) (<= (select arr_0 ?V_43) (select arr_0 ?V_42)))))) (forall ((?V_40 Int)) (=> (and (<= (+ m_0 1) ?V_40) (<= ?V_40 u_0)) (forall ((?V_41 Int)) (=> (and (<= (+ m_0 1) ?V_41) (<= ?V_41 ?V_40)) (<= (select arr_0 ?V_41) (select arr_0 ?V_40))))))))))) ?v_4) (and (< k V_25) (and (and (forall ((?V_38 Int)) (=> (and (<= 0 ?V_38) (<= ?V_38 (- V_25 1))) (forall ((?V_39 Int)) (=> (and (<= 0 ?V_39) (<= ?V_39 ?V_38)) (<= (select buf ?V_39) (select buf ?V_38)))))) (and (forall ((?V_36 Int)) (=> (and (<= l ?V_36) (<= ?V_36 (- ?v_6 1))) (forall ((?V_37 Int)) (=> (and (<= l ?V_37) (<= ?V_37 ?V_36)) (<= (select arr ?V_37) (select arr ?V_36)))))) (and (or (= k 0) (or (= k V_25) (<= (select arr (- ?v_6 1)) ?v_7))) (and (<= 0 k) (and (<= k V_25) (and ?v_8 (and (forall ((?V_35 Int)) (=> (and (<= 0 ?V_35) (<= ?V_35 (- l 1))) (= (select arr ?V_35) (select arr_0 ?V_35)))) (and (forall ((?V_34 Int)) (=> (and (<= (+ u 1) ?V_34) (<= ?V_34 (- V_22 1))) (= (select arr ?V_34) (select arr_0 ?V_34)))) (and ?v_9 (and ?v_10 (and ?v_11 ?v_12))))))))))) (and (and ?v_0 (and ?v_1 (and ?v_2 (and ?v_3 (and (forall ((?V_32 Int)) (=> (and (<= l_0 ?V_32) (<= ?V_32 m_0)) (forall ((?V_33 Int)) (=> (and (<= l_0 ?V_33) (<= ?V_33 ?V_32)) (<= (select arr_0 ?V_33) (select arr_0 ?V_32)))))) (forall ((?V_30 Int)) (=> (and (<= (+ m_0 1) ?V_30) (<= ?V_30 u_0)) (forall ((?V_31 Int)) (=> (and (<= (+ m_0 1) ?V_31) (<= ?V_31 ?V_30)) (<= (select arr_0 ?V_31) (select arr_0 ?V_30))))))))))) ?v_4)))) (or (exists ((?V_28 Int)) (and (and (<= 0 ?V_28) (<= ?V_28 (- V_25 1))) (exists ((?V_29 Int)) (and (and (<= 0 ?V_29) (<= ?V_29 ?V_28)) (> (select buf ?V_29) (select buf ?V_28)))))) (or (exists ((?V_26 Int)) (and (and (<= l ?V_26) (<= ?V_26 (- (+ l ?v_5) 1))) (exists ((?V_27 Int)) (let ((?v_13 (store arr ?v_6 ?v_7))) (and (and (<= l ?V_27) (<= ?V_27 ?V_26)) (> (select ?v_13 ?V_27) (select ?v_13 ?V_26))))))) (or (and (not (= ?v_5 0)) (and (not (= ?v_5 V_25)) (> (select (store arr ?v_6 ?v_7) (- (+ l ?v_5) 1)) (select buf ?v_5)))) (or (> 0 ?v_5) (or (> ?v_5 V_25) (or (not ?v_8) (or (exists ((?V_24 Int)) (and (and (<= 0 ?V_24) (<= ?V_24 (- l 1))) (not (= (select (store arr ?v_6 ?v_7) ?V_24) (select arr_0 ?V_24))))) (or (exists ((?V_23 Int)) (and (and (<= (+ u 1) ?V_23) (<= ?V_23 (- V_22 1))) (not (= (select (store arr ?v_6 ?v_7) ?V_23) (select arr_0 ?V_23))))) (or (not ?v_9) (or (not ?v_10) (or (not ?v_11) (not ?v_12)))))))))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_5 () Int)
(declare-fun a () (Array Int Int))
(assert (let ((?v_0 (and true (>= V_5 0))) (?v_1 (- V_5 1))) (and (and ?v_0 ?v_0) (or (> (- 1) ?v_1) (or (>= ?v_1 V_5) (or (and (< ?v_1 (+ ?v_1 1)) (exists ((?V_8 Int)) (and (and (<= 0 ?V_8) (<= ?V_8 ?v_1)) (exists ((?V_9 Int)) (and (and (<= (+ ?v_1 1) ?V_9) (<= ?V_9 ?v_1)) (> (select a ?V_8) (select a ?V_9))))))) (or (exists ((?V_6 Int)) (and (and (<= ?v_1 ?V_6) (<= ?V_6 ?v_1)) (exists ((?V_7 Int)) (and (and (<= ?v_1 ?V_7) (<= ?V_7 ?V_6)) (> (select a ?V_7) (select a ?V_6)))))) (not (= V_5 V_5)))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_5 () Int)
(declare-fun a () (Array Int Int))
(assert (and (and (forall ((?V_8 Int)) (=> (and (<= 0 ?V_8) (<= ?V_8 (- V_5 1))) (forall ((?V_9 Int)) (=> (and (<= 0 ?V_9) (<= ?V_9 ?V_8)) (<= (select a ?V_9) (select a ?V_8)))))) (>= V_5 0)) (or (or (> 0 0) (or (>= (- V_5 1) V_5) (exists ((?V_6 Int)) (and (and (<= 0 ?V_6) (<= ?V_6 (- V_5 1))) (exists ((?V_7 Int)) (and (and (<= 0 ?V_7) (<= ?V_7 ?V_6)) (> (select a ?V_7) (select a ?V_6)))))))) (< V_5 0))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_6 () Int)
(declare-fun V_5 () Int)
(declare-fun a_0 () (Array Int Int))
(declare-fun t () Int)
(declare-fun ix () Int)
(declare-fun j () Int)
(declare-fun a () (Array Int Int))
(declare-fun i () Int)
(assert (let ((?v_2 (and true (>= V_5 0))) (?v_4 (select a j)) (?v_0 (- i 1))) (let ((?v_1 (= j ?v_0)) (?v_7 (= V_6 V_5)) (?v_3 (- j 1)) (?v_5 (store a (+ j 1) ?v_4))) (let ((?v_6 (not (= ?v_3 ?v_0)))) (and (and ?v_2 (and (> ?v_4 t) (and (>= j 0) (and (and (<= 1 i) (and (< i V_6) (and (<= (- 1) j) (and (<= j ?v_0) (and (forall ((?V_11 Int)) (=> (and (<= 0 ?V_11) (<= ?V_11 ?v_0)) (forall ((?V_12 Int)) (=> (and (<= 0 ?V_12) (<= ?V_12 ?V_11)) (<= (select a ?V_12) (select a ?V_11)))))) (and (or ?v_1 (<= (select a ?v_0) (select a i))) (and (or ?v_1 (forall ((?V_10 Int)) (=> (and (<= (+ j 1) ?V_10) (<= ?V_10 i)) (> (select a ?V_10) t)))) ?v_7))))))) ?v_2)))) (or (> 1 i) (or (>= i V_6) (or (> (- 1) ?v_3) (or (> ?v_3 ?v_0) (or (exists ((?V_8 Int)) (and (and (<= 0 ?V_8) (<= ?V_8 ?v_0)) (exists ((?V_9 Int)) (and (and (<= 0 ?V_9) (<= ?V_9 ?V_8)) (> (select ?v_5 ?V_9) (select ?v_5 ?V_8)))))) (or (and ?v_6 (> (select ?v_5 ?v_0) (select ?v_5 i))) (or (and ?v_6 (exists ((?V_7 Int)) (and (and (<= (+ ?v_3 1) ?V_7) (<= ?V_7 i)) (<= (select ?v_5 ?V_7) t)))) (not ?v_7)))))))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_5 () Int)
(declare-fun l () Int)
(declare-fun e () Int)
(declare-fun a () (Array Int Int))
(declare-fun u () Int)
(declare-fun t_1 () Int)
(assert (let ((?v_0 (select a t_1))) (and (and (< ?v_0 e) (and (not (= ?v_0 e)) (and (and (<= l t_1) (<= t_1 u)) (and (<= l u) (and (and (<= 0 l) (and (< u V_5) (forall ((?V_8 Int)) (=> (and (<= 0 ?V_8) (<= ?V_8 (- V_5 1))) (forall ((?V_9 Int)) (=> (and (<= 0 ?V_9) (<= ?V_9 ?V_8)) (<= (select a ?V_9) (select a ?V_8)))))))) (>= V_5 0)))))) (or (or (> 0 (+ t_1 1)) (or (>= u V_5) (exists ((?V_6 Int)) (and (and (<= 0 ?V_6) (<= ?V_6 (- V_5 1))) (exists ((?V_7 Int)) (and (and (<= 0 ?V_7) (<= ?V_7 ?V_6)) (> (select a ?V_7) (select a ?V_6)))))))) (< V_5 0)))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_3 () Int)
(declare-fun a () (Array Int Int))
(assert (let ((?v_0 (and true (>= V_3 0)))) (and (and ?v_0 ?v_0) (or (> 1 1) (or (exists ((?V_4 Int)) (and (and (<= 0 ?V_4) (<= ?V_4 (- 1 1))) (exists ((?V_5 Int)) (and (and (<= 0 ?V_5) (<= ?V_5 ?V_4)) (> (select a ?V_5) (select a ?V_4)))))) (not (= V_3 V_3)))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_27 () Int)
(declare-fun V_24 () Int)
(declare-fun V_22 () Int)
(declare-fun e () Int)
(declare-fun ix () Int)
(declare-fun buf () (Array Int Int))
(declare-fun a2 () (Array Int Int))
(declare-fun a1 () (Array Int Int))
(assert (let ((?v_0 (and (>= V_22 0) (>= V_24 0))) (?v_2 (= V_27 (+ V_24 V_22))) (?v_1 (> 0 0))) (and (and (and (and (forall ((?V_34 Int)) (=> (and (<= 0 ?V_34) (<= ?V_34 (- V_24 1))) (forall ((?V_35 Int)) (=> (and (<= 0 ?V_35) (<= ?V_35 ?V_34)) (<= (select a1 ?V_35) (select a1 ?V_34)))))) (forall ((?V_32 Int)) (=> (and (<= 0 ?V_32) (<= ?V_32 (- V_22 1))) (forall ((?V_33 Int)) (=> (and (<= 0 ?V_33) (<= ?V_33 ?V_32)) (<= (select a2 ?V_33) (select a2 ?V_32))))))) ?v_0) (and ?v_2 (and (and (forall ((?V_30 Int)) (=> (and (<= 0 ?V_30) (<= ?V_30 (- V_24 1))) (forall ((?V_31 Int)) (=> (and (<= 0 ?V_31) (<= ?V_31 ?V_30)) (<= (select a1 ?V_31) (select a1 ?V_30)))))) (forall ((?V_28 Int)) (=> (and (<= 0 ?V_28) (<= ?V_28 (- V_22 1))) (forall ((?V_29 Int)) (=> (and (<= 0 ?V_29) (<= ?V_29 ?V_28)) (<= (select a2 ?V_29) (select a2 ?V_28))))))) ?v_0))) (or ?v_1 (or (> 0 V_24) (or ?v_1 (or (> 0 V_22) (or ?v_1 (or (> 0 V_27) (or (not (= 0 (+ 0 0))) (or (not ?v_2) (or (not (= V_24 V_24)) (or (not (= V_22 V_22)) (or (exists ((?V_26 Int)) (let ((?v_3 (select a1 ?V_26))) (and (and (<= 0 ?V_26) (<= ?V_26 (- V_24 1))) (not (= ?v_3 ?v_3))))) (or (exists ((?V_25 Int)) (let ((?v_4 (select a2 ?V_25))) (and (and (<= 0 ?V_25) (<= ?V_25 (- V_22 1))) (not (= ?v_4 ?v_4))))) (or (and (not (= 0 V_24)) (exists ((?V_23 Int)) (and (and (<= 0 ?V_23) (<= ?V_23 (- 0 1))) (> (select buf ?V_23) (select a1 0))))) (or (and (not (= 0 V_22)) (exists ((?V_21 Int)) (and (and (<= 0 ?V_21) (<= ?V_21 (- 0 1))) (> (select buf ?V_21) (select a2 0))))) (or (exists ((?V_19 Int)) (and (and (<= 0 ?V_19) (<= ?V_19 (- 0 1))) (exists ((?V_20 Int)) (and (and (<= 0 ?V_20) (<= ?V_20 ?V_19)) (> (select buf ?V_20) (select buf ?V_19)))))) (or (and (or (exists ((?V_18 Int)) (and (and (<= 0 ?V_18) (<= ?V_18 (- 0 1))) (= (select a1 ?V_18) e))) (exists ((?V_17 Int)) (and (and (<= 0 ?V_17) (<= ?V_17 (- 0 1))) (= (select a2 ?V_17) e)))) (forall ((?V_16 Int)) (=> (and (<= 0 ?V_16) (<= ?V_16 (- 0 1))) (not (= (select buf ?V_16) e))))) (and (exists ((?V_15 Int)) (and (and (<= 0 ?V_15) (<= ?V_15 (- 0 1))) (= (select buf ?V_15) e))) (and (forall ((?V_14 Int)) (=> (and (<= 0 ?V_14) (<= ?V_14 (- 0 1))) (not (= (select a1 ?V_14) e)))) (forall ((?V_13 Int)) (=> (and (<= 0 ?V_13) (<= ?V_13 (- 0 1))) (not (= (select a2 ?V_13) e)))))))))))))))))))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_7 () Int)
(declare-fun a () (Array Int Int))
(declare-fun e () Int)
(declare-fun u () Int)
(declare-fun l () Int)
(declare-fun ix () Int)
(assert (let ((?v_0 (<= 0 l)) (?v_1 (< u V_7)) (?v_2 (>= V_7 0))) (and (and (and (and ?v_0 (and ?v_1 (forall ((?V_10 Int)) (=> (and (<= 0 ?V_10) (<= ?V_10 (- V_7 1))) (forall ((?V_11 Int)) (=> (and (<= 0 ?V_11) (<= ?V_11 ?V_10)) (<= (select a ?V_11) (select a ?V_10)))))))) ?v_2) (and (> l u) (and (and ?v_0 (and ?v_1 (forall ((?V_8 Int)) (=> (and (<= 0 ?V_8) (<= ?V_8 (- V_7 1))) (forall ((?V_9 Int)) (=> (and (<= 0 ?V_9) (<= ?V_9 ?V_8)) (<= (select a ?V_9) (select a ?V_8)))))))) ?v_2))) (or (and true (exists ((?V_6 Int)) (and (and (<= l ?V_6) (<= ?V_6 u)) (= (select a ?V_6) e)))) (and false (forall ((?V_5 Int)) (=> (and (<= l ?V_5) (<= ?V_5 u)) (not (= (select a ?V_5) e)))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_8 () Int)
(declare-fun V_7 () Int)
(declare-fun i () Int)
(declare-fun a () (Array Int Int))
(declare-fun a_0 () (Array Int Int))
(assert (let ((?v_0 (and true (>= V_7 0)))) (and (and ?v_0 (and (>= i V_8) (and (and (<= 1 i) (and (forall ((?V_9 Int)) (=> (and (<= 0 ?V_9) (<= ?V_9 (- i 1))) (forall ((?V_10 Int)) (=> (and (<= 0 ?V_10) (<= ?V_10 ?V_9)) (<= (select a ?V_10) (select a ?V_9)))))) (= V_8 V_7))) ?v_0))) (exists ((?V_5 Int)) (and (and (<= 0 ?V_5) (<= ?V_5 (- V_7 1))) (exists ((?V_6 Int)) (and (and (<= 0 ?V_6) (<= ?V_6 ?V_5)) (> (select a ?V_6) (select a ?V_5)))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_26 () Int)
(declare-fun V_24 () Int)
(declare-fun V_23 () Int)
(declare-fun u_0 () Int)
(declare-fun m_0 () Int)
(declare-fun l_0 () Int)
(declare-fun arr_0 () (Array Int Int))
(declare-fun buf () (Array Int Int))
(declare-fun arr () (Array Int Int))
(declare-fun k () Int)
(declare-fun u () Int)
(declare-fun j () Int)
(declare-fun m () Int)
(declare-fun i () Int)
(declare-fun l () Int)
(assert (let ((?v_7 (<= 0 l_0)) (?v_8 (<= l_0 m_0)) (?v_9 (< m_0 u_0)) (?v_10 (< u_0 V_23)) (?v_11 (>= V_23 0)) (?v_6 (select arr j)) (?v_3 (select arr i)) (?v_2 (<= j u)) (?v_1 (<= i m)) (?v_0 (+ m 1)) (?v_13 (+ u 1)) (?v_14 (- i l)) (?v_4 (= k 0)) (?v_16 (> i m)) (?v_5 (select buf (- k 1))) (?v_19 (= V_26 (+ (- u l) 1))) (?v_20 (= V_24 V_23)) (?v_21 (= l l_0)) (?v_22 (= m m_0)) (?v_23 (= u u_0)) (?v_12 (+ j 1)) (?v_15 (+ k 1))) (let ((?v_17 (not (= ?v_15 0))) (?v_18 (select (store buf k ?v_6) (- ?v_15 1)))) (and (and (and (and ?v_7 (and ?v_8 (and ?v_9 (and ?v_10 (and (forall ((?V_46 Int)) (=> (and (<= l_0 ?V_46) (<= ?V_46 m_0)) (forall ((?V_47 Int)) (=> (and (<= l_0 ?V_47) (<= ?V_47 ?V_46)) (<= (select arr_0 ?V_47) (select arr_0 ?V_46)))))) (forall ((?V_44 Int)) (=> (and (<= (+ m_0 1) ?V_44) (<= ?V_44 u_0)) (forall ((?V_45 Int)) (=> (and (<= (+ m_0 1) ?V_45) (<= ?V_45 ?V_44)) (<= (select arr_0 ?V_45) (select arr_0 ?V_44))))))))))) ?v_11) (and (> ?v_3 ?v_6) (and ?v_2 (and ?v_1 (and (< k V_26) (and (and (<= l i) (and (<= i ?v_0) (and (<= ?v_0 j) (and (<= j ?v_13) (and (= k (+ ?v_14 (- j ?v_0))) (and (forall ((?V_42 Int)) (=> (and (<= l ?V_42) (<= ?V_42 m)) (forall ((?V_43 Int)) (=> (and (<= l ?V_43) (<= ?V_43 ?V_42)) (<= (select arr ?V_43) (select arr ?V_42)))))) (and (forall ((?V_40 Int)) (=> (and (<= ?v_0 ?V_40) (<= ?V_40 u)) (forall ((?V_41 Int)) (=> (and (<= ?v_0 ?V_41) (<= ?V_41 ?V_40)) (<= (select arr ?V_41) (select arr ?V_40)))))) (and (or (= k V_26) (or ?v_1 ?v_2)) (and (or ?v_4 (or ?v_16 (<= ?v_5 ?v_3))) (and (or ?v_4 (or (> j u) (<= ?v_5 ?v_6))) (and (forall ((?V_38 Int)) (=> (and (<= 0 ?V_38) (<= ?V_38 (- k 1))) (forall ((?V_39 Int)) (=> (and (<= 0 ?V_39) (<= ?V_39 ?V_38)) (<= (select buf ?V_39) (select buf ?V_38)))))) (and ?v_19 (and (forall ((?V_37 Int)) (=> (and (<= 0 ?V_37) (<= ?V_37 (- V_24 1))) (= (select arr ?V_37) (select arr_0 ?V_37)))) (and ?v_20 (and ?v_21 (and ?v_22 ?v_23)))))))))))))))) (and (and ?v_7 (and ?v_8 (and ?v_9 (and ?v_10 (and (forall ((?V_35 Int)) (=> (and (<= l_0 ?V_35) (<= ?V_35 m_0)) (forall ((?V_36 Int)) (=> (and (<= l_0 ?V_36) (<= ?V_36 ?V_35)) (<= (select arr_0 ?V_36) (select arr_0 ?V_35)))))) (forall ((?V_33 Int)) (=> (and (<= (+ m_0 1) ?V_33) (<= ?V_33 u_0)) (forall ((?V_34 Int)) (=> (and (<= (+ m_0 1) ?V_34) (<= ?V_34 ?V_33)) (<= (select arr_0 ?V_34) (select arr_0 ?V_33))))))))))) ?v_11))))))) (or (> l i) (or (> i ?v_0) (or (> ?v_0 ?v_12) (or (> ?v_12 ?v_13) (or (not (= ?v_15 (+ ?v_14 (- ?v_12 ?v_0)))) (or (exists ((?V_31 Int)) (and (and (<= l ?V_31) (<= ?V_31 m)) (exists ((?V_32 Int)) (and (and (<= l ?V_32) (<= ?V_32 ?V_31)) (> (select arr ?V_32) (select arr ?V_31)))))) (or (exists ((?V_29 Int)) (and (and (<= ?v_0 ?V_29) (<= ?V_29 u)) (exists ((?V_30 Int)) (and (and (<= ?v_0 ?V_30) (<= ?V_30 ?V_29)) (> (select arr ?V_30) (select arr ?V_29)))))) (or (and (not (= ?v_15 V_26)) (and ?v_16 (> ?v_12 u))) (or (and ?v_17 (and ?v_1 (> ?v_18 ?v_3))) (or (and ?v_17 (and (<= ?v_12 u) (> ?v_18 (select arr ?v_12)))) (or (exists ((?V_27 Int)) (and (and (<= 0 ?V_27) (<= ?V_27 (- ?v_15 1))) (exists ((?V_28 Int)) (let ((?v_24 (store buf k ?v_6))) (and (and (<= 0 ?V_28) (<= ?V_28 ?V_27)) (> (select ?v_24 ?V_28) (select ?v_24 ?V_27))))))) (or (not ?v_19) (or (exists ((?V_25 Int)) (and (and (<= 0 ?V_25) (<= ?V_25 (- V_24 1))) (not (= (select arr ?V_25) (select arr_0 ?V_25))))) (or (not ?v_20) (or (not ?v_21) (or (not ?v_22) (not ?v_23)))))))))))))))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun V_9 () Int)
(declare-fun a () (Array Int Int))
(assert (let ((?v_0 (and true (>= V_9 0)))) (and (and ?v_0 ?v_0) (and (forall ((?V_7 Int)) (=> (and (<= 0 ?V_7) (<= ?V_7 1)) (forall ((?V_8 Int)) (let ((?v_1 (store (store a 0 5) 1 7))) (=> (and (<= 0 ?V_8) (<= ?V_8 ?V_7)) (<= (select ?v_1 ?V_8) (select ?v_1 ?V_7))))))) (forall ((?V_5 Int)) (=> (and (<= 0 ?V_5) (<= ?V_5 1)) (forall ((?V_6 Int)) (let ((?v_2 (store (store a 0 1) 1 3))) (=> (and (<= 0 ?V_6) (<= ?V_6 ?V_5)) (<= (select ?v_2 ?V_6) (select ?v_2 ?V_5)))))))))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_6 () Int)
(declare-fun V_5 () Int)
(declare-fun l () Int)
(declare-fun arr () (Array Int Int))
(declare-fun u () Int)
(declare-fun t_2 () (Array Int Int))
(declare-fun t_1 () Int)
(assert (and (and (and (forall ((?V_9 Int)) (=> (and (<= l ?V_9) (<= ?V_9 t_1)) (forall ((?V_10 Int)) (=> (and (<= l ?V_10) (<= ?V_10 ?V_9)) (<= (select t_2 ?V_10) (select t_2 ?V_9)))))) (and (= V_5 V_6) (and (forall ((?V_8 Int)) (=> (and (<= 0 ?V_8) (<= ?V_8 (- l 1))) (= (select t_2 ?V_8) (select arr ?V_8)))) (forall ((?V_7 Int)) (=> (and (<= (+ t_1 1) ?V_7) (<= ?V_7 (- V_6 1))) (= (select t_2 ?V_7) (select arr ?V_7))))))) (and (and (<= l t_1) (< t_1 u)) (and (< l u) (and (and (<= 0 l) (< u V_6)) (>= V_6 0))))) (or (or (> 0 (+ t_1 1)) (>= u V_5)) (< V_5 0))))
(check-sat)
(exit)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_7 () Int)
(declare-fun u () Int)
(declare-fun l () Int)
(declare-fun e () Int)
(declare-fun a () (Array Int Int))
(declare-fun ix () Int)
(declare-fun t_2 () Bool)
(declare-fun t_1 () Int)
(assert (let ((?v_1 (<= 0 l)) (?v_2 (< u V_7)) (?v_3 (>= V_7 0)) (?v_4 (not t_2)) (?v_0 (select a t_1))) (and (and (and (and ?v_1 (and ?v_2 (forall ((?V_12 Int)) (=> (and (<= 0 ?V_12) (<= ?V_12 (- V_7 1))) (forall ((?V_13 Int)) (=> (and (<= 0 ?V_13) (<= ?V_13 ?V_12)) (<= (select a ?V_13) (select a ?V_12)))))))) ?v_3) (and (and (or t_2 (forall ((?V_11 Int)) (=> (and (<= l ?V_11) (<= ?V_11 (- t_1 1))) (not (= (select a ?V_11) e))))) (or ?v_4 (exists ((?V_10 Int)) (and (and (<= l ?V_10) (<= ?V_10 (- t_1 1))) (= (select a ?V_10) e))))) (and (>= ?v_0 e) (and (not (= ?v_0 e)) (and (and (<= l t_1) (<= t_1 u)) (and (<= l u) (and (and ?v_1 (and ?v_2 (forall ((?V_8 Int)) (=> (and (<= 0 ?V_8) (<= ?V_8 (- V_7 1))) (forall ((?V_9 Int)) (=> (and (<= 0 ?V_9) (<= ?V_9 ?V_8)) (<= (select a ?V_9) (select a ?V_8)))))))) ?v_3))))))) (or (and ?v_4 (exists ((?V_6 Int)) (and (and (<= l ?V_6) (<= ?V_6 u)) (= (select a ?V_6) e)))) (and t_2 (forall ((?V_5 Int)) (=> (and (<= l ?V_5) (<= ?V_5 u)) (not (= (select a ?V_5) e)))))))))
(check-sat)
(exit)
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