cvc4 assumptions 72: Y0 : INT; X_ni : INT; Y2 : INT; X_nj : INT; Y3 : INT; Y1 : INT; Y6 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])]; Y7 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])]; Y5 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])]; Y4 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])]; X_uin : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])]; ((EXISTS (t0 : INT, t1 : INT) : (((0) = ((t1) + (-1))) AND (((Y0) = (t0)*(2) + (t1)) AND (((t1) >= 0) AND ((t1) < (2))))))) AND (((0) = ((X_ni) + ((-1) * (Y2)) + (-1)))) AND (((0) = ((X_nj) + ((-1) * (Y3)) + (-1)))) AND (((0) = ((Y0) + ((-1) * (Y2)) + (1)))) AND (((0) = ((Y1) + ((-1) * (Y3)) + (1)))) AND (FORALL (_cc_bv_10__28 : INT) : (FORALL (_cc_bv_11__28 : INT) : ((((0) = (((((Y6).1)[_cc_bv_11__28]).1)[_cc_bv_10__28]))) OR ((0) <= ((X_ni) + ((-1) * (_cc_bv_11__28)) + (-2)))))) AND (FORALL (_cc_bv_10__29 : INT) : (FORALL (_cc_bv_11__29 : INT) : ((((0) = (((((Y6).1)[_cc_bv_11__29]).1)[_cc_bv_10__29]))) OR ((0) <= ((_cc_bv_11__29) + (-1)))))) AND (FORALL (_cc_bv_10__30 : INT) : ((FORALL (_cc_bv_11__30 : INT) : (((0) = (((((Y6).1)[_cc_bv_11__30]).1)[_cc_bv_10__30])))) OR ((0) <= ((X_nj) + ((-1) * (_cc_bv_10__30)) + (-2))))) AND (FORALL (_cc_bv_10__31 : INT) : ((FORALL (_cc_bv_11__31 : INT) : (((0) = (((((Y6).1)[_cc_bv_11__31]).1)[_cc_bv_10__31])))) OR ((0) <= ((_cc_bv_10__31) + (-1))))) AND (FORALL (_cc_bv_14__13 : INT) : (FORALL (_cc_bv_15__13 : INT) : ((((0) = ((Y0) + ((-1) * (_cc_bv_15__13))))) OR (((0) = ((((((Y6).1)[_cc_bv_15__13]).1)[_cc_bv_14__13]) + ((-1) * (((((Y7).1)[_cc_bv_15__13]).1)[_cc_bv_14__13])))))))) AND (FORALL (_cc_bv_14__14 : INT) : ((FORALL (_cc_bv_15__14 : INT) : (((0) = ((((((Y6).1)[_cc_bv_15__14]).1)[_cc_bv_14__14]) + ((-1) * (((((Y7).1)[_cc_bv_15__14]).1)[_cc_bv_14__14])))))) OR ((0) <= ((X_nj) + ((-1) * (_cc_bv_14__14)) + (-2))))) AND (FORALL (_cc_bv_14__15 : INT) : ((FORALL (_cc_bv_15__15 : INT) : (((0) = ((((((Y6).1)[_cc_bv_15__15]).1)[_cc_bv_14__15]) + ((-1) * (((((Y7).1)[_cc_bv_15__15]).1)[_cc_bv_14__15])))))) OR ((0) <= ((_cc_bv_14__15) + (-1))))) AND (FORALL (_cc_bv_18__3 : INT) : (FORALL (_cc_bv_19__3 : INT) : ((((0) = ((((((Y5).1)[_cc_bv_19__3]).1)[_cc_bv_18__3]) + ((-1) * (((((Y7).1)[_cc_bv_19__3]).1)[_cc_bv_18__3]))))) OR ((0) <= ((X_ni) + ((-1) * (_cc_bv_19__3)) + (-2)))))) AND (FORALL (_cc_bv_18__4 : INT) : (FORALL (_cc_bv_19__4 : INT) : ((((0) = ((((((Y5).1)[_cc_bv_19__4]).1)[_cc_bv_18__4]) + ((-1) * (((((Y7).1)[_cc_bv_19__4]).1)[_cc_bv_18__4]))))) OR ((0) <= ((_cc_bv_19__4) + (-1)))))) AND (FORALL (_cc_bv_18__5 : INT) : ((((0) = ((Y1) + ((-1) * (_cc_bv_18__5))))) OR (FORALL (_cc_bv_19__5 : INT) : (((0) = ((((((Y5).1)[_cc_bv_19__5]).1)[_cc_bv_18__5]) + ((-1) * (((((Y7).1)[_cc_bv_19__5]).1)[_cc_bv_18__5])))))))) AND (FORALL (i__27 : INT) : ((((0) = (((((Y4).1)[i__27]).1)[(X_nj) + (-1)]))) OR (((X_ni) + ((-1) * (i__27))) <= (0)) OR (((i__27) + (1)) <= (0)))) AND (FORALL (i__28 : INT) : ((((0) = (((((Y4).1)[i__28]).1)[0]))) OR (((X_ni) + ((-1) * (i__28))) <= (0)) OR (((i__28) + (1)) <= (0)))) AND (FORALL (i__29 : INT) : ((FORALL (j__27 : INT) : ((((0) = (((((((X_uin).1)[i__29]).1)[j__27])^2) + ((-1) * (((((Y4).1)[i__29]).1)[j__27]))))) OR (((X_nj) + ((-1) * (j__27)) + (-1)) <= (0)) OR ((j__27) <= (0)))) OR (((X_ni) + ((-1) * (i__29)) + (-1)) <= (0)) OR ((i__29) <= (0)))) AND (FORALL (j__28 : INT) : ((((0) = (((((Y4).1)[(X_ni) + (-1)]).1)[j__28]))) OR (((X_nj) + ((-1) * (j__28))) <= (0)) OR (((j__28) + (1)) <= (0)))) AND (FORALL (j__29 : INT) : ((((0) = (((((Y4).1)[0]).1)[j__29]))) OR (((X_nj) + ((-1) * (j__29))) <= (0)) OR (((j__29) + (1)) <= (0)))) AND (FORALL (k__26 : INT) : ((FORALL (t__28 : INT) : ((((0) = (((((((X_uin).1)[t__28]).1)[k__26])^2) + ((-1) * (((((Y6).1)[t__28]).1)[k__26]))))) OR (((Y0) + ((-1) * (t__28))) <= (0)) OR ((t__28) <= (0)))) OR ((k__26) <= (0)) OR ((0) <= ((IF ((0) <= ((t3) + (-1))) THEN ((t3) + (-1)) ELSE ((-1) * ((t3) + (-1))) ENDIF) + ((-1) * (X_nj)) + (k__26) + (1))))) AND (FORALL (t__26 : INT) : ((((0) = (((((((X_uin).1)[Y0]).1)[t__26])^2) + ((-1) * (((((Y7).1)[Y0]).1)[t__26]))))) OR (((Y3) + ((-1) * (t__26))) <= (0)) OR ((t__26) <= (0)))) AND (FORALL (t__27 : INT) : ((((0) = (((((((X_uin).1)[t__27]).1)[Y1])^2) + ((-1) * (((((Y5).1)[t__27]).1)[Y1]))))) OR (((Y2) + ((-1) * (t__27))) <= (0)) OR ((t__27) <= (0)))) AND ((0) <= ((X_ni) + (-4))) AND ((0) <= ((X_nj) + (-3))) AND ((0) <= ((Y0) + (-1))) AND ((0) <= ((Y2) + (-1))) AND ((0) <= ((Y3) + (-1))) AND ((((Y0) + (-1)) <= (0)) OR (NOT((EXISTS (t4 : INT, t5 : INT) : (((0) = (t5)) AND (((Y1) = (t4)*(2) + (t5)) AND (((t5) >= 0) AND ((t5) < (2))))))))) cvc4 predicate 72: FORALL (i__30 : INT) : ((FORALL (j__30 : INT) : ((((0) = (((((((Y5).1) WITH [Y0] := ((X_nj,((((Y5).1)[Y0]).1) WITH [Y1] := ((((((X_uin).1)[Y0]).1)[Y1])^2))))[i__30]).1)[j__30]) + ((-1) * (((((Y4).1)[i__30]).1)[j__30]))))) OR (((X_nj) + ((-1) * (j__30))) <= (0)) OR (((j__30) + (1)) <= (0)))) OR (((X_ni) + ((-1) * (i__30))) <= (0)) OR (((i__30) + (1)) <= (0))) cvc4 result 72: MAYBE z3 assumptions 73: (declare-const Y0 Int) (declare-const X_ni Int) (declare-const Y2 Int) (declare-const X_nj Int) (declare-const Y3 Int) (declare-const Y1 Int) (declare-datatypes (T) ((BigArray (mk-BigArray (bigArray-len Int) (bigArray-val (Array Int T)))))) (declare-const Y6 (BigArray (BigArray Real))) (declare-const Y7 (BigArray (BigArray Real))) (declare-const Y5 (BigArray (BigArray Real))) (declare-const Y4 (BigArray (BigArray Real))) (declare-const X_uin (BigArray (BigArray Real))) (let ((t0 (= 0 (+ (mod Y0 2) -1))) ) (let ((t1 (= 0 (+ X_ni (* -1 Y2) -1))) ) (let ((t2 (= 0 (+ X_nj (* -1 Y3) -1))) ) (let ((t3 (= 0 (+ Y0 (* -1 Y2) 1))) ) (let ((t4 (= 0 (+ Y1 (* -1 Y3) 1))) ) (let ((t5 (forall ((_cc_bv_10__28 Int)) (forall ((_cc_bv_11__28 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y6) _cc_bv_11__28)) _cc_bv_10__28)) (<= 0 (+ X_ni (* -1 _cc_bv_11__28) -2)))))) ) (let ((t6 (forall ((_cc_bv_10__29 Int)) (forall ((_cc_bv_11__29 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y6) _cc_bv_11__29)) _cc_bv_10__29)) (<= 0 (+ _cc_bv_11__29 -1)))))) ) (let ((t7 (forall ((_cc_bv_10__30 Int)) (or (forall ((_cc_bv_11__30 Int)) (= 0 (select (bigArray-val (select (bigArray-val Y6) _cc_bv_11__30)) _cc_bv_10__30))) (<= 0 (+ X_nj (* -1 _cc_bv_10__30) -2))))) ) (let ((t8 (forall ((_cc_bv_10__31 Int)) (or (forall ((_cc_bv_11__31 Int)) (= 0 (select (bigArray-val (select (bigArray-val Y6) _cc_bv_11__31)) _cc_bv_10__31))) (<= 0 (+ _cc_bv_10__31 -1))))) ) (let ((t9 (forall ((_cc_bv_14__13 Int)) (forall ((_cc_bv_15__13 Int)) (or (= 0 (+ Y0 (* -1 _cc_bv_15__13))) (= 0 (+ (select (bigArray-val (select (bigArray-val Y6) _cc_bv_15__13)) _cc_bv_14__13) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_15__13)) _cc_bv_14__13)))))))) ) (let ((t10 (forall ((_cc_bv_14__14 Int)) (or (forall ((_cc_bv_15__14 Int)) (= 0 (+ (select (bigArray-val (select (bigArray-val Y6) _cc_bv_15__14)) _cc_bv_14__14) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_15__14)) _cc_bv_14__14))))) (<= 0 (+ X_nj (* -1 _cc_bv_14__14) -2))))) ) (let ((t11 (forall ((_cc_bv_14__15 Int)) (or (forall ((_cc_bv_15__15 Int)) (= 0 (+ (select (bigArray-val (select (bigArray-val Y6) _cc_bv_15__15)) _cc_bv_14__15) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_15__15)) _cc_bv_14__15))))) (<= 0 (+ _cc_bv_14__15 -1))))) ) (let ((t12 (forall ((_cc_bv_18__3 Int)) (forall ((_cc_bv_19__3 Int)) (or (= 0 (+ (select (bigArray-val (select (bigArray-val Y5) _cc_bv_19__3)) _cc_bv_18__3) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_19__3)) _cc_bv_18__3)))) (<= 0 (+ X_ni (* -1 _cc_bv_19__3) -2)))))) ) (let ((t13 (forall ((_cc_bv_18__4 Int)) (forall ((_cc_bv_19__4 Int)) (or (= 0 (+ (select (bigArray-val (select (bigArray-val Y5) _cc_bv_19__4)) _cc_bv_18__4) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_19__4)) _cc_bv_18__4)))) (<= 0 (+ _cc_bv_19__4 -1)))))) ) (let ((t14 (forall ((_cc_bv_18__5 Int)) (or (= 0 (+ Y1 (* -1 _cc_bv_18__5))) (forall ((_cc_bv_19__5 Int)) (= 0 (+ (select (bigArray-val (select (bigArray-val Y5) _cc_bv_19__5)) _cc_bv_18__5) (* -1 (select (bigArray-val (select (bigArray-val Y7) _cc_bv_19__5)) _cc_bv_18__5)))))))) ) (let ((t15 (forall ((i__27 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y4) i__27)) (+ X_nj -1))) (<= (+ X_ni (* -1 i__27)) 0) (<= (+ i__27 1) 0)))) ) (let ((t16 (forall ((i__28 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y4) i__28)) 0)) (<= (+ X_ni (* -1 i__28)) 0) (<= (+ i__28 1) 0)))) ) (let ((t17 (forall ((i__29 Int)) (or (forall ((j__27 Int)) (or (= 0 (+ (^ (select (bigArray-val (select (bigArray-val X_uin) i__29)) j__27) 2) (* -1 (select (bigArray-val (select (bigArray-val Y4) i__29)) j__27)))) (<= (+ X_nj (* -1 j__27) -1) 0) (<= j__27 0))) (<= (+ X_ni (* -1 i__29) -1) 0) (<= i__29 0)))) ) (let ((t18 (forall ((j__28 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y4) (+ X_ni -1))) j__28)) (<= (+ X_nj (* -1 j__28)) 0) (<= (+ j__28 1) 0)))) ) (let ((t19 (forall ((j__29 Int)) (or (= 0 (select (bigArray-val (select (bigArray-val Y4) 0)) j__29)) (<= (+ X_nj (* -1 j__29)) 0) (<= (+ j__29 1) 0)))) ) (let ((t20 (forall ((k__26 Int)) (or (forall ((t__28 Int)) (or (= 0 (+ (^ (select (bigArray-val (select (bigArray-val X_uin) t__28)) k__26) 2) (* -1 (select (bigArray-val (select (bigArray-val Y6) t__28)) k__26)))) (<= (+ Y0 (* -1 t__28)) 0) (<= t__28 0))) (<= k__26 0) (<= 0 (+ (ite (<= 0 (+ (mod (+ X_nj -3) 2) -1)) (+ (mod (+ X_nj -3) 2) -1) (* -1 (+ (mod (+ X_nj -3) 2) -1))) (* -1 X_nj) k__26 1))))) ) (let ((t21 (forall ((t__26 Int)) (or (= 0 (+ (^ (select (bigArray-val (select (bigArray-val X_uin) Y0)) t__26) 2) (* -1 (select (bigArray-val (select (bigArray-val Y7) Y0)) t__26)))) (<= (+ Y3 (* -1 t__26)) 0) (<= t__26 0)))) ) (let ((t22 (forall ((t__27 Int)) (or (= 0 (+ (^ (select (bigArray-val (select (bigArray-val X_uin) t__27)) Y1) 2) (* -1 (select (bigArray-val (select (bigArray-val Y5) t__27)) Y1)))) (<= (+ Y2 (* -1 t__27)) 0) (<= t__27 0)))) ) (let ((t23 (or (<= (+ Y0 -1) 0) (not (= 0 (mod Y1 2))))) ) (let ((t24 (and t0 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 t16 t17 t18 t19 t20 t21 t22 (<= 0 (+ X_ni -4)) (<= 0 (+ X_nj -3)) (<= 0 (+ Y0 -1)) (<= 0 (+ Y2 -1)) (<= 0 (+ Y3 -1)) t23)) ) t24))))))))))))))))))))))))) z3 predicate 73: (declare-datatypes (T) ((BigArray (mk-BigArray (bigArray-len Int) (bigArray-val (Array Int T)))))) (forall ((i__30 Int)) (or (forall ((j__30 Int)) (or (= 0 (+ (select (bigArray-val (select (store (bigArray-val Y5) Y0 (mk-BigArray X_nj (store (bigArray-val (select (bigArray-val Y5) Y0)) Y1 (^ (select (bigArray-val (select (bigArray-val X_uin) Y0)) Y1) 2)))) i__30)) j__30) (* -1 (select (bigArray-val (select (bigArray-val Y4) i__30)) j__30)))) (<= (+ X_nj (* -1 j__30)) 0) (<= (+ j__30 1) 0))) (<= (+ X_ni (* -1 i__30)) 0) (<= (+ i__30 1) 0))) z3 result 73: MAYBE cvc3 assumptions 74: Y0 : INT; X_ni : INT; Y2 : INT; X_nj : INT; Y3 : INT; Y1 : INT; Y6 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])]; Y7 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])]; Y5 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])]; Y4 : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])]; X_uin : [INT, ARRAY INT OF ([INT, ARRAY INT OF (REAL)])]; ((EXISTS (t0 : INT, t1 : INT) : (((0) = ((t1) + (-1))) AND (((Y0) = (t0)*(2) + (t1)) AND (((t1) >= 0) AND ((t1) < (2))))))) AND (((0) = ((X_ni) + ((-1) * (Y2)) + (-1)))) AND (((0) = ((X_nj) + ((-1) * (Y3)) + (-1)))) AND (((0) = ((Y0) + ((-1) * (Y2)) + (1)))) AND (((0) = ((Y1) + ((-1) * (Y3)) + (1)))) AND (FORALL (_cc_bv_10__28 : INT) : (FORALL (_cc_bv_11__28 : INT) : ((((0) = (((((Y6).1)[_cc_bv_11__28]).1)[_cc_bv_10__28]))) OR ((0) <= ((X_ni) + ((-1) * (_cc_bv_11__28)) + (-2)))))) AND (FORALL (_cc_bv_10__29 : INT) : (FORALL (_cc_bv_11__29 : INT) : ((((0) = (((((Y6).1)[_cc_bv_11__29]).1)[_cc_bv_10__29]))) OR ((0) <= ((_cc_bv_11__29) + (-1)))))) AND (FORALL (_cc_bv_10__30 : INT) : ((FORALL (_cc_bv_11__30 : INT) : (((0) = (((((Y6).1)[_cc_bv_11__30]).1)[_cc_bv_10__30])))) OR ((0) <= ((X_nj) + ((-1) * (_cc_bv_10__30)) + (-2))))) AND (FORALL (_cc_bv_10__31 : INT) : ((FORALL (_cc_bv_11__31 : INT) : (((0) = (((((Y6).1)[_cc_bv_11__31]).1)[_cc_bv_10__31])))) OR ((0) <= ((_cc_bv_10__31) + (-1))))) AND (FORALL (_cc_bv_14__13 : INT) : (FORALL (_cc_bv_15__13 : INT) : ((((0) = ((Y0) + ((-1) * (_cc_bv_15__13))))) OR (((0) = ((((((Y6).1)[_cc_bv_15__13]).1)[_cc_bv_14__13]) + ((-1) * (((((Y7).1)[_cc_bv_15__13]).1)[_cc_bv_14__13])))))))) AND (FORALL (_cc_bv_14__14 : INT) : ((FORALL (_cc_bv_15__14 : INT) : (((0) = ((((((Y6).1)[_cc_bv_15__14]).1)[_cc_bv_14__14]) + ((-1) * (((((Y7).1)[_cc_bv_15__14]).1)[_cc_bv_14__14])))))) OR ((0) <= ((X_nj) + ((-1) * (_cc_bv_14__14)) + (-2))))) AND (FORALL (_cc_bv_14__15 : INT) : ((FORALL (_cc_bv_15__15 : INT) : (((0) = ((((((Y6).1)[_cc_bv_15__15]).1)[_cc_bv_14__15]) + ((-1) * (((((Y7).1)[_cc_bv_15__15]).1)[_cc_bv_14__15])))))) OR ((0) <= ((_cc_bv_14__15) + (-1))))) AND (FORALL (_cc_bv_18__3 : INT) : (FORALL (_cc_bv_19__3 : INT) : ((((0) = ((((((Y5).1)[_cc_bv_19__3]).1)[_cc_bv_18__3]) + ((-1) * (((((Y7).1)[_cc_bv_19__3]).1)[_cc_bv_18__3]))))) OR ((0) <= ((X_ni) + ((-1) * (_cc_bv_19__3)) + (-2)))))) AND (FORALL (_cc_bv_18__4 : INT) : (FORALL (_cc_bv_19__4 : INT) : ((((0) = ((((((Y5).1)[_cc_bv_19__4]).1)[_cc_bv_18__4]) + ((-1) * (((((Y7).1)[_cc_bv_19__4]).1)[_cc_bv_18__4]))))) OR ((0) <= ((_cc_bv_19__4) + (-1)))))) AND (FORALL (_cc_bv_18__5 : INT) : ((((0) = ((Y1) + ((-1) * (_cc_bv_18__5))))) OR (FORALL (_cc_bv_19__5 : INT) : (((0) = ((((((Y5).1)[_cc_bv_19__5]).1)[_cc_bv_18__5]) + ((-1) * (((((Y7).1)[_cc_bv_19__5]).1)[_cc_bv_18__5])))))))) AND (FORALL (i__27 : INT) : ((((0) = (((((Y4).1)[i__27]).1)[(X_nj) + (-1)]))) OR (((X_ni) + ((-1) * (i__27))) <= (0)) OR (((i__27) + (1)) <= (0)))) AND (FORALL (i__28 : INT) : ((((0) = (((((Y4).1)[i__28]).1)[0]))) OR (((X_ni) + ((-1) * (i__28))) <= (0)) OR (((i__28) + (1)) <= (0)))) AND (FORALL (i__29 : INT) : ((FORALL (j__27 : INT) : ((((0) = (((((((X_uin).1)[i__29]).1)[j__27])^2) + ((-1) * (((((Y4).1)[i__29]).1)[j__27]))))) OR (((X_nj) + ((-1) * (j__27)) + (-1)) <= (0)) OR ((j__27) <= (0)))) OR (((X_ni) + ((-1) * (i__29)) + (-1)) <= (0)) OR ((i__29) <= (0)))) AND (FORALL (j__28 : INT) : ((((0) = (((((Y4).1)[(X_ni) + (-1)]).1)[j__28]))) OR (((X_nj) + ((-1) * (j__28))) <= (0)) OR (((j__28) + (1)) <= (0)))) AND (FORALL (j__29 : INT) : ((((0) = (((((Y4).1)[0]).1)[j__29]))) OR (((X_nj) + ((-1) * (j__29))) <= (0)) OR (((j__29) + (1)) <= (0)))) AND (FORALL (k__26 : INT) : ((FORALL (t__28 : INT) : ((((0) = (((((((X_uin).1)[t__28]).1)[k__26])^2) + ((-1) * (((((Y6).1)[t__28]).1)[k__26]))))) OR (((Y0) + ((-1) * (t__28))) <= (0)) OR ((t__28) <= (0)))) OR ((k__26) <= (0)) OR ((0) <= ((IF ((0) <= ((t3) + (-1))) THEN ((t3) + (-1)) ELSE ((-1) * ((t3) + (-1))) ENDIF) + ((-1) * (X_nj)) + (k__26) + (1))))) AND (FORALL (t__26 : INT) : ((((0) = (((((((X_uin).1)[Y0]).1)[t__26])^2) + ((-1) * (((((Y7).1)[Y0]).1)[t__26]))))) OR (((Y3) + ((-1) * (t__26))) <= (0)) OR ((t__26) <= (0)))) AND (FORALL (t__27 : INT) : ((((0) = (((((((X_uin).1)[t__27]).1)[Y1])^2) + ((-1) * (((((Y5).1)[t__27]).1)[Y1]))))) OR (((Y2) + ((-1) * (t__27))) <= (0)) OR ((t__27) <= (0)))) AND ((0) <= ((X_ni) + (-4))) AND ((0) <= ((X_nj) + (-3))) AND ((0) <= ((Y0) + (-1))) AND ((0) <= ((Y2) + (-1))) AND ((0) <= ((Y3) + (-1))) AND ((((Y0) + (-1)) <= (0)) OR (NOT((EXISTS (t4 : INT, t5 : INT) : (((0) = (t5)) AND (((Y1) = (t4)*(2) + (t5)) AND (((t5) >= 0) AND ((t5) < (2))))))))) cvc3 predicate 74: FORALL (i__30 : INT) : ((FORALL (j__30 : INT) : ((((0) = (((((((Y5).1) WITH [Y0] := ((X_nj,((((Y5).1)[Y0]).1) WITH [Y1] := ((((((X_uin).1)[Y0]).1)[Y1])^2))))[i__30]).1)[j__30]) + ((-1) * (((((Y4).1)[i__30]).1)[j__30]))))) OR (((X_nj) + ((-1) * (j__30))) <= (0)) OR (((j__30) + (1)) <= (0)))) OR (((X_ni) + ((-1) * (i__30))) <= (0)) OR (((i__30) + (1)) <= (0))) cvc3 result 74: MAYBE theory SARL_REAL use import real.Real function add (a b : real) : real = a + b function sub (a b : real) : real = a - b function mul (a b : real) : real = a * b function neg (a : real) : real = (-a) function (:-) (a b : real) : real = a / b predicate lt (a b : real) = a < b predicate lte (a b : real) = a <= b clone import int.Exponentiation as POWREAL with type t = real function sarl_power (a : real) (b : int) : real = (POWREAL.power a b) use import real.PowerReal as POWREALREAL function sarl_power_real (a : real) (b : real) : real = (POWREALREAL.pow a b) end theory Why3Query_75 use import int.EuclideanDivision use import map.Map use import int.Int use import SARL_REAL as SR constant _Y0 : int constant _X_ni : int constant _Y2 : int constant _X_nj : int constant _Y3 : int constant _Y1 : int constant _Y6 : (map int (map int real)) constant _Y7 : (map int (map int real)) constant _Y5 : (map int (map int real)) constant _Y4 : (map int (map int real)) constant _X_uin : (map int (map int real)) predicate _Axcontext = (((0) = ((mod _Y0 (2)) + (-1))) && ((0) = (_X_ni + ((-1) * _Y2) + (-1))) && ((0) = (_X_nj + ((-1) * _Y3) + (-1))) && ((0) = (_Y0 + ((-1) * _Y2) + (1))) && ((0) = (_Y1 + ((-1) * _Y3) + (1))) && (forall __cc_bv_10__28 : int. (forall __cc_bv_11__28 : int. ((0.0 = (get (get _Y6 __cc_bv_11__28) __cc_bv_10__28)) || ((0) <= (_X_ni + ((-1) * __cc_bv_11__28) + (-2)))))) && (forall __cc_bv_10__29 : int. (forall __cc_bv_11__29 : int. ((0.0 = (get (get _Y6 __cc_bv_11__29) __cc_bv_10__29)) || ((0) <= (__cc_bv_11__29 + (-1)))))) && (forall __cc_bv_10__30 : int. ((forall __cc_bv_11__30 : int. (0.0 = (get (get _Y6 __cc_bv_11__30) __cc_bv_10__30))) || ((0) <= (_X_nj + ((-1) * __cc_bv_10__30) + (-2))))) && (forall __cc_bv_10__31 : int. ((forall __cc_bv_11__31 : int. (0.0 = (get (get _Y6 __cc_bv_11__31) __cc_bv_10__31))) || ((0) <= (__cc_bv_10__31 + (-1))))) && (forall __cc_bv_14__13 : int. (forall __cc_bv_15__13 : int. (((0) = (_Y0 + ((-1) * __cc_bv_15__13))) || (0.0 = ( SR.add (get (get _Y6 __cc_bv_15__13) __cc_bv_14__13) ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_15__13) __cc_bv_14__13))))))) && (forall __cc_bv_14__14 : int. ((forall __cc_bv_15__14 : int. (0.0 = ( SR.add (get (get _Y6 __cc_bv_15__14) __cc_bv_14__14) ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_15__14) __cc_bv_14__14))))) || ((0) <= (_X_nj + ((-1) * __cc_bv_14__14) + (-2))))) && (forall __cc_bv_14__15 : int. ((forall __cc_bv_15__15 : int. (0.0 = ( SR.add (get (get _Y6 __cc_bv_15__15) __cc_bv_14__15) ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_15__15) __cc_bv_14__15))))) || ((0) <= (__cc_bv_14__15 + (-1))))) && (forall __cc_bv_18__3 : int. (forall __cc_bv_19__3 : int. ((0.0 = ( SR.add (get (get _Y5 __cc_bv_19__3) __cc_bv_18__3) ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_19__3) __cc_bv_18__3)))) || ((0) <= (_X_ni + ((-1) * __cc_bv_19__3) + (-2)))))) && (forall __cc_bv_18__4 : int. (forall __cc_bv_19__4 : int. ((0.0 = ( SR.add (get (get _Y5 __cc_bv_19__4) __cc_bv_18__4) ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_19__4) __cc_bv_18__4)))) || ((0) <= (__cc_bv_19__4 + (-1)))))) && (forall __cc_bv_18__5 : int. (((0) = (_Y1 + ((-1) * __cc_bv_18__5))) || (forall __cc_bv_19__5 : int. (0.0 = ( SR.add (get (get _Y5 __cc_bv_19__5) __cc_bv_18__5) ( SR.mul (SR.neg 1.0) (get (get _Y7 __cc_bv_19__5) __cc_bv_18__5))))))) && (forall _i__27 : int. ((0.0 = (get (get _Y4 _i__27) (_X_nj + (-1)))) || ((_X_ni + ((-1) * _i__27)) <= (0)) || ((_i__27 + (1)) <= (0)))) && (forall _i__28 : int. ((0.0 = (get (get _Y4 _i__28) (0))) || ((_X_ni + ((-1) * _i__28)) <= (0)) || ((_i__28 + (1)) <= (0)))) && (forall _i__29 : int. ((forall _j__27 : int. ((0.0 = ( SR.add (SR.mul (get (get _X_uin _i__29) _j__27) (get (get _X_uin _i__29) _j__27)) ( SR.mul (SR.neg 1.0) (get (get _Y4 _i__29) _j__27)))) || ((_X_nj + ((-1) * _j__27) + (-1)) <= (0)) || (_j__27 <= (0)))) || ((_X_ni + ((-1) * _i__29) + (-1)) <= (0)) || (_i__29 <= (0)))) && (forall _j__28 : int. ((0.0 = (get (get _Y4 (_X_ni + (-1))) _j__28)) || ((_X_nj + ((-1) * _j__28)) <= (0)) || ((_j__28 + (1)) <= (0)))) && (forall _j__29 : int. ((0.0 = (get (get _Y4 (0)) _j__29)) || ((_X_nj + ((-1) * _j__29)) <= (0)) || ((_j__29 + (1)) <= (0)))) && (forall _k__26 : int. ((forall _t__28 : int. ((0.0 = ( SR.add (SR.mul (get (get _X_uin _t__28) _k__26) (get (get _X_uin _t__28) _k__26)) ( SR.mul (SR.neg 1.0) (get (get _Y6 _t__28) _k__26)))) || ((_Y0 + ((-1) * _t__28)) <= (0)) || (_t__28 <= (0)))) || (_k__26 <= (0)) || ((0) <= ((if ((0) <= ((mod (_X_nj + (-3)) (2)) + (-1))) then ((mod (_X_nj + (-3)) (2)) + (-1)) else ((-1) * ((mod (_X_nj + (-3)) (2)) + (-1)))) + ((-1) * _X_nj) + _k__26 + (1))))) && (forall _t__26 : int. ((0.0 = ( SR.add (SR.mul (get (get _X_uin _Y0) _t__26) (get (get _X_uin _Y0) _t__26)) ( SR.mul (SR.neg 1.0) (get (get _Y7 _Y0) _t__26)))) || ((_Y3 + ((-1) * _t__26)) <= (0)) || (_t__26 <= (0)))) && (forall _t__27 : int. ((0.0 = ( SR.add (SR.mul (get (get _X_uin _t__27) _Y1) (get (get _X_uin _t__27) _Y1)) ( SR.mul (SR.neg 1.0) (get (get _Y5 _t__27) _Y1)))) || ((_Y2 + ((-1) * _t__27)) <= (0)) || (_t__27 <= (0)))) && ((0) <= (_X_ni + (-4))) && ((0) <= (_X_nj + (-3))) && ((0) <= (_Y0 + (-1))) && ((0) <= (_Y2 + (-1))) && ((0) <= (_Y3 + (-1))) && (((_Y0 + (-1)) <= (0)) || (not ((0) = (mod _Y1 (2)))))) predicate context = _Axcontext goal G0: context -> (forall _i__30 : int. ((forall _j__30 : int. ((0.0 = ( SR.add (get (get (set _Y5 _Y0 (set (get _Y5 _Y0) _Y1 (SR.mul (get (get _X_uin _Y0) _Y1) (get (get _X_uin _Y0) _Y1)))) _i__30) _j__30) ( SR.mul (SR.neg 1.0) (get (get _Y4 _i__30) _j__30)))) || ((_X_nj + ((-1) * _j__30)) <= (0)) || ((_j__30 + (1)) <= (0)))) || ((_X_ni + ((-1) * _i__30)) <= (0)) || ((_i__30 + (1)) <= (0)))) end