swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
Raw File
Tip revision: f94b06de7edcb61d3c49f19417e53dc7dc21d552 authored by Anish Tondwalkar on 22 June 2021, 08:13:54 UTC
updated README
Tip revision: f94b06d
pointersMap_noalias.smt2
(set-logic HORN)
(set-info :source |
  Benchmark: /home/atondwal/src/mist/mochi-tests/pointersMap_noalias.ml
  Generated by MoCHi
|)
(set-info :status unknown)
(declare-fun |fail_103[0:0]| ( Int) Bool)
(declare-fun |k_test[0:3]| ( Int  Int  Bool) Bool)
(declare-fun |thenn[0:2][0:0][0:1][0:1][0:1][0:0]| ( Int  Int  Int) Bool)
(declare-fun |thenn[0:1][0:1][0:1][0:1][0:0]| ( Int  Int  Int) Bool)
(declare-fun |zero[0:1][0:0][0:1][0:1][0:1][0:0]| ( Int  Int  Int  Int) Bool)
(declare-fun |bind[0:3][0:1][0:1][0:0]| ( Int  Int  Int) Bool)
(declare-fun |bind[0:1][0:1][0:0][0:1][0:1][0:1][0:0]| ( Int  Int  Int) Bool)
(declare-fun |bind[0:1][0:1][0:0][0:0][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |bind[0:0][0:1][0:1][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |bind[0:0][0:1][0:1][0:0]| ( Int) Bool)
(declare-fun |bind[0:1][0:1][0:0][0:0][0:0]| ( Int) Bool)
(declare-fun |bind[0:1][0:1][0:0][0:1][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |bind[0:3][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |zero[0:1][0:0][0:1][0:1][0:0]| ( Int  Int  Int) Bool)
(declare-fun |thenn[0:1][0:1][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |thenn[0:2][0:0][0:1][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |thenn[0:2][0:0][0:1][0:0]| ( Int) Bool)
(declare-fun |thenn[0:1][0:1][0:0]| ( Int) Bool)
(declare-fun |zero[0:1][0:0][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |bind[0:3][0:0]| ( Int) Bool)
(declare-fun |bind[0:1][0:1][0:0][0:1][0:0]| ( Int) Bool)
(declare-fun |bind[0:1][0:0][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |bind[0:0][0:1][0:0][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |bind[0:0][0:0][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |bind[0:2][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |zero[0:1][0:0][0:0][0:1][0:0]| ( Int  Int  Int) Bool)
(declare-fun |thenn[0:1][0:0][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |thenn[0:0][0:1][0:1][0:1][0:0]| ( Int  Int  Int) Bool)
(declare-fun |thenn[0:0][0:1][0:1][0:0]| ( Int  Int) Bool)
(declare-fun |thenn[0:0][0:1][0:0]| ( Int) Bool)
(declare-fun |thenn[0:1][0:0][0:0]| ( Int) Bool)
(declare-fun |zero[0:1][0:0][0:0][0:0]| ( Int  Int) Bool)
(declare-fun |bind[0:2][0:0]| ( Int) Bool)
(declare-fun |bind[0:0][0:0][0:0]| ( Int) Bool)
(declare-fun |bind[0:0][0:1][0:0][0:0]| ( Int) Bool)
(declare-fun |bind[0:1][0:0][0:0]| ( Int) Bool)
(declare-fun |zero[0:0]| ( Int) Bool)
(assert (not (exists ((x0 Int)) (|fail_103[0:0]| x0))))
(assert (forall ((x0 Int)(x1 Int)(x2 Int)) (=> (|k_test[0:3]| x1 x2 false) (|fail_103[0:0]| x0))))
(assert (forall ((x1 Int)(x2 Int)(x0 Bool)(x3 Int)) (=> (and (|bind[0:1][0:0][0:1][0:0]| 0 x3) (and (not (= x3 0)) (and (>= x1 0) (and (>= x2 0) (not x0))))) (|k_test[0:3]| x1 x2 x0))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:0][0:1][0:0][0:1][0:0]| x0 x1) (|bind[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)(x3 Int)) (=> (|bind[0:0][0:0][0:1][0:0]| x2 x3) (|bind[0:0][0:1][0:0][0:1][0:0]| x2 x3))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:2][0:1][0:0]| x0 x1) (|bind[0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)(x3 Int)) (=> (|thenn[0:1][0:0][0:1][0:0]| x2 x3) (|bind[0:2][0:1][0:0]| x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(var9390 Int)) (=> (and (|thenn[0:0][0:1][0:1][0:1][0:0]| var9390 x0 x1) (|thenn[0:0][0:1][0:0]| var9390)) (|thenn[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x4) (and (|thenn[0:2][0:0][0:1][0:1][0:1][0:0]| x4 x2 x3) (|thenn[0:2][0:0][0:1][0:0]| x4))) (|thenn[0:0][0:1][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x2 Int)(x0 Int)(x1 Int)(var9392 Int)) (=> (and (|thenn[0:2][0:0][0:1][0:0]| x2) (and (|thenn[0:1][0:1][0:1][0:1][0:0]| x2 x0 x1) (and (|thenn[0:1][0:1][0:0]| x2) (|thenn[0:0][0:1][0:0]| var9392)))) (|thenn[0:2][0:0][0:1][0:1][0:1][0:0]| x2 x0 x1))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|thenn[0:1][0:1][0:0]| x4) (and (|zero[0:1][0:0][0:1][0:1][0:1][0:0]| 1 x4 x2 x3) (|zero[0:1][0:0][0:1][0:0]| 1 x4))) (|thenn[0:1][0:1][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x2 Int)(x3 Int)(x0 Int)(x1 Int)) (=> (and (|zero[0:0]| x2) (and (|bind[0:3][0:0]| x3) (and (|bind[0:3][0:1][0:1][0:0]| x3 x0 x1) (|zero[0:1][0:0][0:1][0:0]| x2 x3)))) (|zero[0:1][0:0][0:1][0:1][0:1][0:0]| x2 x3 x0 x1))))
(assert (forall ((x2 Int)(x0 Int)(x1 Int)) (=> (and (|bind[0:3][0:0]| x2) (and (|bind[0:1][0:1][0:0][0:1][0:1][0:1][0:0]| x2 x0 x1) (|bind[0:1][0:1][0:0][0:1][0:0]| x2))) (|bind[0:3][0:1][0:1][0:0]| x2 x0 x1))))
(assert (forall ((x3 Int)(x1 Int)(x2 Int)(var9394 Int)(x0 Int)) (=> (and (|bind[0:1][0:1][0:0][0:1][0:0]| x3) (and (|bind[0:1][0:1][0:0][0:0][0:1][0:0]| x1 x2) (and (|zero[0:0]| x0) (and (|bind[0:1][0:0][0:1][0:0]| x0 var9394) (<= var9394 0))))) (|bind[0:1][0:1][0:0][0:1][0:1][0:1][0:0]| x3 x1 x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:0][0:1][0:1][0:1][0:0]| x0 x1) (|bind[0:1][0:1][0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|bind[0:0][0:0][0:1][0:0]| x1 x2) (|zero[0:0]| x0)) (|bind[0:0][0:1][0:1][0:1][0:0]| x1 x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:2][0:1][0:0]| x0 x1) (|bind[0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|zero[0:0]| x0) (|zero[0:1][0:0][0:0][0:1][0:0]| x0 x1 x2)) (|bind[0:2][0:1][0:0]| x1 x2))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|zero[0:0]| x4) (and (|thenn[0:1][0:0][0:1][0:0]| x2 x3) (= x4 1))) (|zero[0:1][0:0][0:0][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(var9396 Int)) (=> (and (|thenn[0:0][0:1][0:1][0:1][0:0]| var9396 x0 x1) (|thenn[0:0][0:1][0:0]| var9396)) (|thenn[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x4) (and (|thenn[0:2][0:0][0:1][0:1][0:1][0:0]| x4 x2 x3) (|thenn[0:2][0:0][0:1][0:0]| x4))) (|thenn[0:0][0:1][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x2 Int)(x0 Int)(x1 Int)(var9398 Int)) (=> (and (|thenn[0:2][0:0][0:1][0:0]| x2) (and (|thenn[0:1][0:1][0:1][0:1][0:0]| x2 x0 x1) (and (|thenn[0:1][0:1][0:0]| x2) (|thenn[0:0][0:1][0:0]| var9398)))) (|thenn[0:2][0:0][0:1][0:1][0:1][0:0]| x2 x0 x1))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|thenn[0:1][0:1][0:0]| x4) (and (|zero[0:1][0:0][0:1][0:1][0:1][0:0]| 0 x4 x2 x3) (|zero[0:1][0:0][0:1][0:0]| 0 x4))) (|thenn[0:1][0:1][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x2 Int)(x3 Int)(x0 Int)(x1 Int)) (=> (and (|zero[0:0]| x2) (and (|bind[0:3][0:0]| x3) (and (|bind[0:3][0:1][0:1][0:0]| x3 x0 x1) (|zero[0:1][0:0][0:1][0:0]| x2 x3)))) (|zero[0:1][0:0][0:1][0:1][0:1][0:0]| x2 x3 x0 x1))))
(assert (forall ((x2 Int)(x0 Int)(x1 Int)) (=> (and (|bind[0:3][0:0]| x2) (and (|bind[0:1][0:1][0:0][0:1][0:1][0:1][0:0]| x2 x0 x1) (|bind[0:1][0:1][0:0][0:1][0:0]| x2))) (|bind[0:3][0:1][0:1][0:0]| x2 x0 x1))))
(assert (forall ((x3 Int)(x1 Int)(x2 Int)(var9400 Int)(x0 Int)) (=> (and (|bind[0:1][0:1][0:0][0:1][0:0]| x3) (and (|bind[0:1][0:1][0:0][0:0][0:1][0:0]| x1 x2) (and (|zero[0:0]| x0) (and (|bind[0:1][0:0][0:1][0:0]| x0 var9400) (<= var9400 0))))) (|bind[0:1][0:1][0:0][0:1][0:1][0:1][0:0]| x3 x1 x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:0][0:1][0:1][0:1][0:0]| x0 x1) (|bind[0:1][0:1][0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|bind[0:0][0:0][0:1][0:0]| x1 x2) (|zero[0:0]| x0)) (|bind[0:0][0:1][0:1][0:1][0:0]| x1 x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:2][0:1][0:0]| x0 x1) (|bind[0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|zero[0:0]| x0) (|zero[0:1][0:0][0:0][0:1][0:0]| x0 x1 x2)) (|bind[0:2][0:1][0:0]| x1 x2))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|zero[0:0]| x4) (and (|thenn[0:1][0:0][0:1][0:0]| x2 x3) (= x4 0))) (|zero[0:1][0:0][0:0][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(var9402 Int)) (=> (and (|thenn[0:0][0:1][0:1][0:1][0:0]| var9402 x0 x1) (|thenn[0:0][0:1][0:0]| var9402)) (|thenn[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)(var9403 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x4) (and (|thenn[0:0][0:1][0:1][0:0]| var9403 x2) (and (|bind[0:1][0:0][0:1][0:0]| x2 x3) (and (not (= x2 0)) (not (= x2 1)))))) (|thenn[0:0][0:1][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:0][0:1][0:0][0:1][0:0]| x0 x1) (|bind[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)(x3 Int)) (=> (|bind[0:0][0:0][0:1][0:0]| x2 x3) (|bind[0:0][0:1][0:0][0:1][0:0]| x2 x3))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:2][0:1][0:0]| x0 x1) (|bind[0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)(x3 Int)) (=> (|bind[0:2][0:0]| x2) (|bind[0:2][0:1][0:0]| x2 x3))))
(assert (forall ((x0 Int)) (=> (|bind[0:0][0:0][0:0]| x0) (|bind[0:2][0:0]| x0))))
(assert (forall ((x2 Int)) (=> (|bind[0:0][0:1][0:0][0:0]| x2) (|bind[0:0][0:0][0:0]| x2))))
(assert (forall ((x0 Int)) (=> (|bind[0:1][0:0][0:0]| x0) (|bind[0:0][0:1][0:0][0:0]| x0))))
(assert (forall ((x2 Int)(var9404 Int)) (=> (and (|thenn[0:0][0:1][0:1][0:0]| var9404 x2) (and (not (= x2 0)) (not (= x2 1)))) (|bind[0:1][0:0][0:0]| x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x0) (|thenn[0:1][0:0][0:0]| x1)) (|thenn[0:0][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)) (=> (|zero[0:1][0:0][0:0][0:0]| 0 x2) (|thenn[0:1][0:0][0:0]| x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|zero[0:0]| x0) (|bind[0:2][0:0]| x1)) (|zero[0:1][0:0][0:0][0:0]| x0 x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:0][0:0][0:0]| x0) (|bind[0:2][0:0]| x0))))
(assert (forall ((x1 Int)(x0 Int)) (=> (and (|bind[0:0][0:1][0:1][0:0]| x1) (|zero[0:0]| x0)) (|bind[0:0][0:0][0:0]| x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:1][0:1][0:0][0:0][0:0]| x0) (|bind[0:0][0:1][0:1][0:0]| x0))))
(assert (forall ((x1 Int)(var9407 Int)(var9406 Int)(x0 Int)) (=> (and (|bind[0:1][0:1][0:0][0:1][0:1][0:0]| var9406 x1) (and (|bind[0:1][0:0][0:1][0:0]| x0 var9407) (and (|zero[0:0]| x0) (<= var9407 0)))) (|bind[0:1][0:1][0:0][0:0][0:0]| x1))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:3][0:1][0:0]| x0 x1) (|bind[0:1][0:1][0:0][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|zero[0:0]| x0) (|zero[0:1][0:0][0:1][0:1][0:0]| x0 x1 x2)) (|bind[0:3][0:1][0:0]| x1 x2))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|zero[0:0]| x4) (and (|thenn[0:1][0:1][0:1][0:0]| x2 x3) (= x4 0))) (|zero[0:1][0:0][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(var9408 Int)) (=> (and (|thenn[0:2][0:0][0:1][0:1][0:0]| x0 x1) (|thenn[0:0][0:1][0:0]| var9408)) (|thenn[0:1][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)(x3 Int)) (=> (|thenn[0:0][0:1][0:1][0:0]| x2 x3) (|thenn[0:2][0:0][0:1][0:1][0:0]| x2 x3))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x0) (|thenn[0:1][0:0][0:0]| x1)) (|thenn[0:0][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)) (=> (|zero[0:1][0:0][0:0][0:0]| 1 x2) (|thenn[0:1][0:0][0:0]| x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|zero[0:0]| x0) (|bind[0:2][0:0]| x1)) (|zero[0:1][0:0][0:0][0:0]| x0 x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:0][0:0][0:0]| x0) (|bind[0:2][0:0]| x0))))
(assert (forall ((x1 Int)(x0 Int)) (=> (and (|bind[0:0][0:1][0:1][0:0]| x1) (|zero[0:0]| x0)) (|bind[0:0][0:0][0:0]| x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:1][0:1][0:0][0:0][0:0]| x0) (|bind[0:0][0:1][0:1][0:0]| x0))))
(assert (forall ((x1 Int)(var9411 Int)(var9410 Int)(x0 Int)) (=> (and (|bind[0:1][0:1][0:0][0:1][0:1][0:0]| var9410 x1) (and (|bind[0:1][0:0][0:1][0:0]| x0 var9411) (and (|zero[0:0]| x0) (<= var9411 0)))) (|bind[0:1][0:1][0:0][0:0][0:0]| x1))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:3][0:1][0:0]| x0 x1) (|bind[0:1][0:1][0:0][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|zero[0:0]| x0) (|zero[0:1][0:0][0:1][0:1][0:0]| x0 x1 x2)) (|bind[0:3][0:1][0:0]| x1 x2))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|zero[0:0]| x4) (and (|thenn[0:1][0:1][0:1][0:0]| x2 x3) (= x4 1))) (|zero[0:1][0:0][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(var9412 Int)) (=> (and (|thenn[0:2][0:0][0:1][0:1][0:0]| x0 x1) (|thenn[0:0][0:1][0:0]| var9412)) (|thenn[0:1][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)(x3 Int)) (=> (|thenn[0:0][0:1][0:1][0:0]| x2 x3) (|thenn[0:2][0:0][0:1][0:1][0:0]| x2 x3))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x0) (|thenn[0:1][0:0][0:0]| x1)) (|thenn[0:0][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)) (=> (|bind[0:2][0:0]| x2) (|thenn[0:1][0:0][0:0]| x2))))
(assert (forall ((x0 Int)) (=> (|bind[0:0][0:0][0:0]| x0) (|bind[0:2][0:0]| x0))))
(assert (forall ((x2 Int)) (=> (|bind[0:0][0:1][0:0][0:0]| x2) (|bind[0:0][0:0][0:0]| x2))))
(assert (forall ((x0 Int)) (=> (|bind[0:1][0:0][0:0]| x0) (|bind[0:0][0:1][0:0][0:0]| x0))))
(assert (forall ((x2 Int)) (=> (= x2 0) (|bind[0:1][0:0][0:0]| x2))))
(assert (forall ((x2 Int)) (=> (|thenn[0:2][0:0][0:1][0:0]| x2) (|thenn[0:0][0:1][0:0]| x2))))
(assert (forall ((x0 Int)(var9413 Int)) (=> (and (|thenn[0:1][0:1][0:0]| x0) (|thenn[0:0][0:1][0:0]| var9413)) (|thenn[0:2][0:0][0:1][0:0]| x0))))
(assert (forall ((x2 Int)) (=> (|zero[0:1][0:0][0:1][0:0]| 1 x2) (|thenn[0:1][0:1][0:0]| x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|zero[0:0]| x0) (|bind[0:3][0:0]| x1)) (|zero[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:1][0:1][0:0][0:1][0:0]| x0) (|bind[0:3][0:0]| x0))))
(assert (forall ((x1 Int)(var9414 Int)(x0 Int)) (=> (and (|bind[0:1][0:0][0:1][0:0]| x0 var9414) (and (|zero[0:0]| x0) (<= var9414 0))) (|bind[0:1][0:1][0:0][0:1][0:0]| x1))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:0][0:1][0:0][0:1][0:0]| x0 x1) (|bind[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|bind[0:0][0:0][0:1][0:0]| x1 x2) (|zero[0:0]| x0)) (|bind[0:0][0:1][0:0][0:1][0:0]| x1 x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:2][0:1][0:0]| x0 x1) (|bind[0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|zero[0:0]| x0) (|zero[0:1][0:0][0:0][0:1][0:0]| x0 x1 x2)) (|bind[0:2][0:1][0:0]| x1 x2))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|zero[0:0]| x4) (and (|thenn[0:1][0:0][0:1][0:0]| x2 x3) (= x4 1))) (|zero[0:1][0:0][0:0][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(var9416 Int)) (=> (and (|thenn[0:0][0:1][0:1][0:1][0:0]| var9416 x0 x1) (|thenn[0:0][0:1][0:0]| var9416)) (|thenn[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x4) (and (|thenn[0:2][0:0][0:1][0:1][0:1][0:0]| x4 x2 x3) (|thenn[0:2][0:0][0:1][0:0]| x4))) (|thenn[0:0][0:1][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x2 Int)(x0 Int)(x1 Int)(var9418 Int)) (=> (and (|thenn[0:2][0:0][0:1][0:0]| x2) (and (|thenn[0:1][0:1][0:1][0:1][0:0]| x2 x0 x1) (and (|thenn[0:1][0:1][0:0]| x2) (|thenn[0:0][0:1][0:0]| var9418)))) (|thenn[0:2][0:0][0:1][0:1][0:1][0:0]| x2 x0 x1))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|thenn[0:1][0:1][0:0]| x4) (and (|zero[0:1][0:0][0:1][0:1][0:1][0:0]| 0 x4 x2 x3) (|zero[0:1][0:0][0:1][0:0]| 0 x4))) (|thenn[0:1][0:1][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x2 Int)(x3 Int)(x0 Int)(x1 Int)) (=> (and (|zero[0:0]| x2) (and (|bind[0:3][0:0]| x3) (and (|bind[0:3][0:1][0:1][0:0]| x3 x0 x1) (|zero[0:1][0:0][0:1][0:0]| x2 x3)))) (|zero[0:1][0:0][0:1][0:1][0:1][0:0]| x2 x3 x0 x1))))
(assert (forall ((x2 Int)(x0 Int)(x1 Int)) (=> (and (|bind[0:3][0:0]| x2) (and (|bind[0:1][0:1][0:0][0:1][0:1][0:1][0:0]| x2 x0 x1) (|bind[0:1][0:1][0:0][0:1][0:0]| x2))) (|bind[0:3][0:1][0:1][0:0]| x2 x0 x1))))
(assert (forall ((x3 Int)(x1 Int)(x2 Int)(var9420 Int)(x0 Int)) (=> (and (|bind[0:1][0:1][0:0][0:1][0:0]| x3) (and (|bind[0:1][0:1][0:0][0:0][0:1][0:0]| x1 x2) (and (|zero[0:0]| x0) (and (|bind[0:1][0:0][0:1][0:0]| x0 var9420) (<= var9420 0))))) (|bind[0:1][0:1][0:0][0:1][0:1][0:1][0:0]| x3 x1 x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:0][0:1][0:1][0:1][0:0]| x0 x1) (|bind[0:1][0:1][0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|bind[0:0][0:0][0:1][0:0]| x1 x2) (|zero[0:0]| x0)) (|bind[0:0][0:1][0:1][0:1][0:0]| x1 x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:2][0:1][0:0]| x0 x1) (|bind[0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|zero[0:0]| x0) (|zero[0:1][0:0][0:0][0:1][0:0]| x0 x1 x2)) (|bind[0:2][0:1][0:0]| x1 x2))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|zero[0:0]| x4) (and (|thenn[0:1][0:0][0:1][0:0]| x2 x3) (= x4 0))) (|zero[0:1][0:0][0:0][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(var9422 Int)) (=> (and (|thenn[0:0][0:1][0:1][0:1][0:0]| var9422 x0 x1) (|thenn[0:0][0:1][0:0]| var9422)) (|thenn[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)(var9423 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x4) (and (|thenn[0:0][0:1][0:1][0:0]| var9423 x2) (and (|bind[0:1][0:0][0:1][0:0]| x2 x3) (and (not (= x2 0)) (not (= x2 1)))))) (|thenn[0:0][0:1][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:0][0:1][0:0][0:1][0:0]| x0 x1) (|bind[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)(x3 Int)) (=> (|bind[0:0][0:0][0:1][0:0]| x2 x3) (|bind[0:0][0:1][0:0][0:1][0:0]| x2 x3))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:2][0:1][0:0]| x0 x1) (|bind[0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)(x3 Int)) (=> (|bind[0:2][0:0]| x2) (|bind[0:2][0:1][0:0]| x2 x3))))
(assert (forall ((x0 Int)) (=> (|bind[0:0][0:0][0:0]| x0) (|bind[0:2][0:0]| x0))))
(assert (forall ((x2 Int)) (=> (|bind[0:0][0:1][0:0][0:0]| x2) (|bind[0:0][0:0][0:0]| x2))))
(assert (forall ((x0 Int)) (=> (|bind[0:1][0:0][0:0]| x0) (|bind[0:0][0:1][0:0][0:0]| x0))))
(assert (forall ((x2 Int)(var9424 Int)) (=> (and (|thenn[0:0][0:1][0:1][0:0]| var9424 x2) (and (not (= x2 0)) (not (= x2 1)))) (|bind[0:1][0:0][0:0]| x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x0) (|thenn[0:1][0:0][0:0]| x1)) (|thenn[0:0][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)) (=> (|zero[0:1][0:0][0:0][0:0]| 0 x2) (|thenn[0:1][0:0][0:0]| x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|zero[0:0]| x0) (|bind[0:2][0:0]| x1)) (|zero[0:1][0:0][0:0][0:0]| x0 x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:0][0:0][0:0]| x0) (|bind[0:2][0:0]| x0))))
(assert (forall ((x1 Int)(x0 Int)) (=> (and (|bind[0:0][0:1][0:1][0:0]| x1) (|zero[0:0]| x0)) (|bind[0:0][0:0][0:0]| x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:1][0:1][0:0][0:0][0:0]| x0) (|bind[0:0][0:1][0:1][0:0]| x0))))
(assert (forall ((x1 Int)(var9427 Int)(var9426 Int)(x0 Int)) (=> (and (|bind[0:1][0:1][0:0][0:1][0:1][0:0]| var9426 x1) (and (|bind[0:1][0:0][0:1][0:0]| x0 var9427) (and (|zero[0:0]| x0) (<= var9427 0)))) (|bind[0:1][0:1][0:0][0:0][0:0]| x1))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:3][0:1][0:0]| x0 x1) (|bind[0:1][0:1][0:0][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|zero[0:0]| x0) (|zero[0:1][0:0][0:1][0:1][0:0]| x0 x1 x2)) (|bind[0:3][0:1][0:0]| x1 x2))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|zero[0:0]| x4) (and (|thenn[0:1][0:1][0:1][0:0]| x2 x3) (= x4 0))) (|zero[0:1][0:0][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(var9428 Int)) (=> (and (|thenn[0:2][0:0][0:1][0:1][0:0]| x0 x1) (|thenn[0:0][0:1][0:0]| var9428)) (|thenn[0:1][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)(x3 Int)) (=> (|thenn[0:0][0:1][0:1][0:0]| x2 x3) (|thenn[0:2][0:0][0:1][0:1][0:0]| x2 x3))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x0) (|thenn[0:1][0:0][0:0]| x1)) (|thenn[0:0][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)) (=> (|zero[0:1][0:0][0:0][0:0]| 1 x2) (|thenn[0:1][0:0][0:0]| x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|zero[0:0]| x0) (|bind[0:2][0:0]| x1)) (|zero[0:1][0:0][0:0][0:0]| x0 x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:0][0:0][0:0]| x0) (|bind[0:2][0:0]| x0))))
(assert (forall ((x1 Int)(x0 Int)) (=> (and (|bind[0:0][0:1][0:0][0:0]| x1) (|zero[0:0]| x0)) (|bind[0:0][0:0][0:0]| x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:1][0:0][0:0]| x0) (|bind[0:0][0:1][0:0][0:0]| x0))))
(assert (forall ((x1 Int)) (=> (|zero[0:0]| x1) (|bind[0:1][0:0][0:0]| x1))))
(assert (forall ((x2 Int)) (=> (|thenn[0:2][0:0][0:1][0:0]| x2) (|thenn[0:0][0:1][0:0]| x2))))
(assert (forall ((x0 Int)(var9430 Int)) (=> (and (|thenn[0:1][0:1][0:0]| x0) (|thenn[0:0][0:1][0:0]| var9430)) (|thenn[0:2][0:0][0:1][0:0]| x0))))
(assert (forall ((x2 Int)) (=> (|zero[0:1][0:0][0:1][0:0]| 0 x2) (|thenn[0:1][0:1][0:0]| x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|zero[0:0]| x0) (|bind[0:3][0:0]| x1)) (|zero[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:1][0:1][0:0][0:1][0:0]| x0) (|bind[0:3][0:0]| x0))))
(assert (forall ((x1 Int)(var9431 Int)(x0 Int)) (=> (and (|bind[0:1][0:0][0:1][0:0]| x0 var9431) (and (|zero[0:0]| x0) (<= var9431 0))) (|bind[0:1][0:1][0:0][0:1][0:0]| x1))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:0][0:1][0:0][0:1][0:0]| x0 x1) (|bind[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|bind[0:0][0:0][0:1][0:0]| x1 x2) (|zero[0:0]| x0)) (|bind[0:0][0:1][0:0][0:1][0:0]| x1 x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (|bind[0:2][0:1][0:0]| x0 x1) (|bind[0:0][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x1 Int)(x2 Int)(x0 Int)) (=> (and (|zero[0:0]| x0) (|zero[0:1][0:0][0:0][0:1][0:0]| x0 x1 x2)) (|bind[0:2][0:1][0:0]| x1 x2))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)) (=> (and (|zero[0:0]| x4) (and (|thenn[0:1][0:0][0:1][0:0]| x2 x3) (= x4 0))) (|zero[0:1][0:0][0:0][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)(var9433 Int)) (=> (and (|thenn[0:0][0:1][0:1][0:1][0:0]| var9433 x0 x1) (|thenn[0:0][0:1][0:0]| var9433)) (|thenn[0:1][0:0][0:1][0:0]| x0 x1))))
(assert (forall ((x4 Int)(x2 Int)(x3 Int)(var9434 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x4) (and (|thenn[0:0][0:1][0:1][0:0]| var9434 x2) (and (= x2 0) (>= x3 0)))) (|thenn[0:0][0:1][0:1][0:1][0:0]| x4 x2 x3))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|thenn[0:0][0:1][0:0]| x0) (|thenn[0:1][0:0][0:0]| x1)) (|thenn[0:0][0:1][0:1][0:0]| x0 x1))))
(assert (forall ((x2 Int)) (=> (|zero[0:1][0:0][0:0][0:0]| 0 x2) (|thenn[0:1][0:0][0:0]| x2))))
(assert (forall ((x0 Int)(x1 Int)) (=> (and (|zero[0:0]| x0) (|bind[0:2][0:0]| x1)) (|zero[0:1][0:0][0:0][0:0]| x0 x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:0][0:0][0:0]| x0) (|bind[0:2][0:0]| x0))))
(assert (forall ((x1 Int)(x0 Int)) (=> (and (|bind[0:0][0:1][0:0][0:0]| x1) (|zero[0:0]| x0)) (|bind[0:0][0:0][0:0]| x1))))
(assert (forall ((x0 Int)) (=> (|bind[0:1][0:0][0:0]| x0) (|bind[0:0][0:1][0:0][0:0]| x0))))
(assert (forall ((x1 Int)) (=> (|zero[0:0]| x1) (|bind[0:1][0:0][0:0]| x1))))
(assert (forall ((x2 Int)) (|thenn[0:0][0:1][0:0]| x2)))
(assert (forall ((x0 Int)) (=> (= x0 0) (|zero[0:0]| x0))))
(assert (forall ((x0 Int)) (=> (= x0 1) (|zero[0:0]| x0))))
(check-sat)
(get-model)
(exit)
back to top