gistfile1.txt

(get-info :version)
; (:version "4.3.2")
; (set-option :print-success true) ; Boogie: false
(set-option :global-decls true) ; Boogie: default
(set-option :auto_config false) ; Usually a good idea
(set-option :smt.mbqi false)
(set-option :model false)
(set-option :model.v2 true)
; (set-option :produce-models true)
; (set-option :model.compact true)
(set-option :smt.phase_selection 0)
(set-option :smt.restart_strategy 0)
(set-option :smt.restart_factor |1.5|)
(set-option :smt.arith.random_initial_value true)
(set-option :smt.case_split 3)
(set-option :smt.delay_units true)
(set-option :smt.delay_units_threshold 16)
(set-option :nnf.sk_hack true)
(set-option :smt.qi.eager_threshold 100)
(set-option :smt.qi.cost "(+ weight generation)")
(set-option :type_check true)
(set-option :smt.bv.reflect true)
(set-option :sat.random_seed 0)
; (set-option :combined_solver.solver2_timeout 100)
; (set-option :smt.refine_inj_axioms false)
(declare-datatypes () ((
    $Snap $Snap.unit
    ($Snap.combine ($Snap.first $Snap) ($Snap.second $Snap)))))
(declare-sort $Ref)
(declare-const $Ref.null $Ref)
(define-sort $Perm () Real)
(define-const $Perm.Write $Perm 1.0)
(define-const $Perm.No $Perm 0.0)
(define-fun $Perm.isValidVar ((p $Perm)) Bool
	(<= $Perm.No p))
(define-fun $Perm.isReadVar ((p $Perm) (ub $Perm)) Bool
    (and ($Perm.isValidVar p)
         (not (= p $Perm.No))
         (< p $Perm.Write)))
(define-fun $Perm.min ((p1 $Perm) (p2 $Perm)) Real
    (ite (<= p1 p2) p1 p2))
(define-fun $Math.min ((a Int) (b Int)) Int
    (ite (<= a b) a b))
(define-fun $Math.clip ((a Int)) Int
    (ite (< a 0) 0 a))
(push) ; 1
(declare-sort $Seq<$Ref>)
(declare-sort $Seq<Int>)
(declare-sort $Set<$Seq<$Ref>>)
(declare-sort $Set<Int>)
(declare-sort $Set<$Ref>)
(declare-sort $FVF<$Ref>)
(declare-sort $FVF<$Seq<$Ref>>)
(declare-sort $FVF<Int>)
; /dafny_axioms/sets_declarations_dafny.smt2 [Seq[Ref]]
(declare-fun $Set.in ($Seq<$Ref> $Set<$Seq<$Ref>>) Bool)
(declare-fun $Set.card ($Set<$Seq<$Ref>>) Int)
(declare-fun $Set.empty<$Seq<$Ref>> () $Set<$Seq<$Ref>>)
(declare-fun $Set.singleton ($Seq<$Ref>) $Set<$Seq<$Ref>>)
(declare-fun $Set.unionone ($Set<$Seq<$Ref>> $Seq<$Ref>) $Set<$Seq<$Ref>>)
(declare-fun $Set.union ($Set<$Seq<$Ref>> $Set<$Seq<$Ref>>) $Set<$Seq<$Ref>>)
(declare-fun $Set.disjoint ($Set<$Seq<$Ref>> $Set<$Seq<$Ref>>) Bool)
(declare-fun $Set.difference ($Set<$Seq<$Ref>> $Set<$Seq<$Ref>>) $Set<$Seq<$Ref>>)
(declare-fun $Set.intersection ($Set<$Seq<$Ref>> $Set<$Seq<$Ref>>) $Set<$Seq<$Ref>>)
(declare-fun $Set.subset ($Set<$Seq<$Ref>> $Set<$Seq<$Ref>>) Bool)
(declare-fun $Set.equal ($Set<$Seq<$Ref>> $Set<$Seq<$Ref>>) Bool)
; /dafny_axioms/sets_declarations_dafny.smt2 [Int]
(declare-fun $Set.in (Int $Set<Int>) Bool)
(declare-fun $Set.card ($Set<Int>) Int)
(declare-fun $Set.empty<Int> () $Set<Int>)
(declare-fun $Set.singleton (Int) $Set<Int>)
(declare-fun $Set.unionone ($Set<Int> Int) $Set<Int>)
(declare-fun $Set.union ($Set<Int> $Set<Int>) $Set<Int>)
(declare-fun $Set.disjoint ($Set<Int> $Set<Int>) Bool)
(declare-fun $Set.difference ($Set<Int> $Set<Int>) $Set<Int>)
(declare-fun $Set.intersection ($Set<Int> $Set<Int>) $Set<Int>)
(declare-fun $Set.subset ($Set<Int> $Set<Int>) Bool)
(declare-fun $Set.equal ($Set<Int> $Set<Int>) Bool)
; /dafny_axioms/sets_declarations_dafny.smt2 [Ref]
(declare-fun $Set.in ($Ref $Set<$Ref>) Bool)
(declare-fun $Set.card ($Set<$Ref>) Int)
(declare-fun $Set.empty<$Ref> () $Set<$Ref>)
(declare-fun $Set.singleton ($Ref) $Set<$Ref>)
(declare-fun $Set.unionone ($Set<$Ref> $Ref) $Set<$Ref>)
(declare-fun $Set.union ($Set<$Ref> $Set<$Ref>) $Set<$Ref>)
(declare-fun $Set.disjoint ($Set<$Ref> $Set<$Ref>) Bool)
(declare-fun $Set.difference ($Set<$Ref> $Set<$Ref>) $Set<$Ref>)
(declare-fun $Set.intersection ($Set<$Ref> $Set<$Ref>) $Set<$Ref>)
(declare-fun $Set.subset ($Set<$Ref> $Set<$Ref>) Bool)
(declare-fun $Set.equal ($Set<$Ref> $Set<$Ref>) Bool)
; /dafny_axioms/sequences_declarations_dafny.smt2 [Ref]
(declare-fun $Seq.length ($Seq<$Ref>) Int)
(declare-fun $Seq.empty<$Ref> () $Seq<$Ref>)
(declare-fun $Seq.singleton ($Ref) $Seq<$Ref>)
(declare-fun $Seq.build ($Seq<$Ref> $Ref) $Seq<$Ref>)
(declare-fun $Seq.index ($Seq<$Ref> Int) $Ref)
(declare-fun $Seq.append ($Seq<$Ref> $Seq<$Ref>) $Seq<$Ref>)
(declare-fun $Seq.update ($Seq<$Ref> Int $Ref) $Seq<$Ref>)
(declare-fun $Seq.contains ($Seq<$Ref> $Ref) Bool)
(declare-fun $Seq.take ($Seq<$Ref> Int) $Seq<$Ref>)
(declare-fun $Seq.drop ($Seq<$Ref> Int) $Seq<$Ref>)
(declare-fun $Seq.equal ($Seq<$Ref> $Seq<$Ref>) Bool)
(declare-fun $Seq.sameuntil ($Seq<$Ref> $Seq<$Ref> Int) Bool)
; /dafny_axioms/sequences_declarations_dafny.smt2 [Int]
(declare-fun $Seq.length ($Seq<Int>) Int)
(declare-fun $Seq.empty<Int> () $Seq<Int>)
(declare-fun $Seq.singleton (Int) $Seq<Int>)
(declare-fun $Seq.build ($Seq<Int> Int) $Seq<Int>)
(declare-fun $Seq.index ($Seq<Int> Int) Int)
(declare-fun $Seq.append ($Seq<Int> $Seq<Int>) $Seq<Int>)
(declare-fun $Seq.update ($Seq<Int> Int Int) $Seq<Int>)
(declare-fun $Seq.contains ($Seq<Int> Int) Bool)
(declare-fun $Seq.take ($Seq<Int> Int) $Seq<Int>)
(declare-fun $Seq.drop ($Seq<Int> Int) $Seq<Int>)
(declare-fun $Seq.equal ($Seq<Int> $Seq<Int>) Bool)
(declare-fun $Seq.sameuntil ($Seq<Int> $Seq<Int> Int) Bool)
; /dafny_axioms/sequences_int_declarations_dafny.smt2
(declare-fun $Seq.range (Int Int) $Seq<Int>)
(assert true)
; /field_value_functions_declarations.smt2 [dst: Seq[Ref]]
(declare-fun $FVF.domain_dst ($FVF<$Seq<$Ref>>) $Set<$Ref>)
(declare-fun $FVF.lookup_dst ($FVF<$Seq<$Ref>> $Ref) $Seq<$Ref>)
; /field_value_functions_declarations.smt2 [src: Seq[Ref]]
(declare-fun $FVF.domain_src ($FVF<$Seq<$Ref>>) $Set<$Ref>)
(declare-fun $FVF.lookup_src ($FVF<$Seq<$Ref>> $Ref) $Seq<$Ref>)
; /field_value_functions_declarations.smt2 [Integer_value: Int]
(declare-fun $FVF.domain_Integer_value ($FVF<Int>) $Set<$Ref>)
(declare-fun $FVF.lookup_Integer_value ($FVF<Int> $Ref) Int)
; /dafny_axioms/sequences_axioms_dafny.smt2 [Ref]
(assert (forall ((s $Seq<$Ref>) ) (! (<= 0 ($Seq.length s))
  :pattern ( ($Seq.length s))
  )))
(assert (= ($Seq.length $Seq.empty<$Ref>) 0))
(assert (forall ((s $Seq<$Ref>) ) (! (=> (= ($Seq.length s) 0) (= s $Seq.empty<$Ref>))
  :pattern ( ($Seq.length s))
  )))
(assert (forall ((t $Ref) ) (! (= ($Seq.length ($Seq.singleton t)) 1)
  :pattern ( ($Seq.length ($Seq.singleton t)))
  )))
(assert (forall ((s $Seq<$Ref>) (v $Ref) ) (! (= ($Seq.length ($Seq.build s v)) (+ 1 ($Seq.length s)))
  :pattern ( ($Seq.length ($Seq.build s v)))
  )))
(assert (forall ((s $Seq<$Ref>) (i Int) (v $Ref) ) (! (and
  (=> (= i ($Seq.length s)) (= ($Seq.index ($Seq.build s v) i) v))
  (=> (not (= i ($Seq.length s))) (= ($Seq.index ($Seq.build s v) i) ($Seq.index s i))))
  :pattern ( ($Seq.index ($Seq.build s v) i))
  )))
(assert (forall ((s0 $Seq<$Ref>) (s1 $Seq<$Ref>) ) (! (= ($Seq.length ($Seq.append s0 s1)) (+ ($Seq.length s0) ($Seq.length s1)))
  :pattern ( ($Seq.length ($Seq.append s0 s1)))
  )))
(assert (forall ((t $Ref) ) (! (= ($Seq.index ($Seq.singleton t) 0) t)
  :pattern ( ($Seq.index ($Seq.singleton t) 0))
  )))
(assert (forall ((s0 $Seq<$Ref>) (s1 $Seq<$Ref>) (n Int) ) (! (and
  (=> (< n ($Seq.length s0)) (= ($Seq.index ($Seq.append s0 s1) n) ($Seq.index s0 n)))
  (=> (<= ($Seq.length s0) n) (= ($Seq.index ($Seq.append s0 s1) n) ($Seq.index s1 (- n ($Seq.length s0))))))
  :pattern ( ($Seq.index ($Seq.append s0 s1) n))
  )))
(assert (forall ((s $Seq<$Ref>) (i Int) (v $Ref) ) (! (=> (and
  (<= 0 i)
  (< i ($Seq.length s))) (= ($Seq.length ($Seq.update s i v)) ($Seq.length s)))
  :pattern ( ($Seq.length ($Seq.update s i v)))
  )))
(assert (forall ((s $Seq<$Ref>) (i Int) (v $Ref) (n Int) ) (! (=> (and
  (<= 0 n)
  (< n ($Seq.length s))) (and
  (=> (= i n) (= ($Seq.index ($Seq.update s i v) n) v))
  (=> (not (= i n)) (= ($Seq.index ($Seq.update s i v) n) ($Seq.index s n)))))
  :pattern ( ($Seq.index ($Seq.update s i v) n))
  )))
(assert (forall ((s $Seq<$Ref>) (x $Ref) ) (! (and
  (=> ($Seq.contains s x) (exists ((i Int) ) (! (and
  (<= 0 i)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )))
  (=> (exists ((i Int) ) (! (and
  (<= 0 i)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )) ($Seq.contains s x)))
  :pattern ( ($Seq.contains s x))
  )))
(assert (forall ((x $Ref) ) (! (not ($Seq.contains $Seq.empty<$Ref> x))
  :pattern ( ($Seq.contains $Seq.empty<$Ref> x))
  )))
(assert (forall ((s0 $Seq<$Ref>) (s1 $Seq<$Ref>) (x $Ref) ) (! (and
  (=> ($Seq.contains ($Seq.append s0 s1) x) (or
  ($Seq.contains s0 x)
  ($Seq.contains s1 x)))
  (=> (or
  ($Seq.contains s0 x)
  ($Seq.contains s1 x)) ($Seq.contains ($Seq.append s0 s1) x)))
  :pattern ( ($Seq.contains ($Seq.append s0 s1) x))
  )))
(assert (forall ((s $Seq<$Ref>) (v $Ref) (x $Ref) ) (! (and
  (=> ($Seq.contains ($Seq.build s v) x) (or
  (= v x)
  ($Seq.contains s x)))
  (=> (or
  (= v x)
  ($Seq.contains s x)) ($Seq.contains ($Seq.build s v) x)))
  :pattern ( ($Seq.contains ($Seq.build s v) x))
  )))
(assert (forall ((s $Seq<$Ref>) (n Int) (x $Ref) ) (! (and
  (=> ($Seq.contains ($Seq.take s n) x) (exists ((i Int) ) (! (and
  (<= 0 i)
  (< i n)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )))
  (=> (exists ((i Int) ) (! (and
  (<= 0 i)
  (< i n)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )) ($Seq.contains ($Seq.take s n) x)))
  :pattern ( ($Seq.contains ($Seq.take s n) x))
  )))
(assert (forall ((s $Seq<$Ref>) (n Int) (x $Ref) ) (! (and
  (=> ($Seq.contains ($Seq.drop s n) x) (exists ((i Int) ) (! (and
  (<= 0 n)
  (<= n i)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )))
  (=> (exists ((i Int) ) (! (and
  (<= 0 n)
  (<= n i)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )) ($Seq.contains ($Seq.drop s n) x)))
  :pattern ( ($Seq.contains ($Seq.drop s n) x))
  )))
(assert (forall ((s0 $Seq<$Ref>) (s1 $Seq<$Ref>) ) (! (and
  (=> ($Seq.equal s0 s1) (and
  (= ($Seq.length s0) ($Seq.length s1))
  (forall ((j Int) ) (! (=> (and
  (<= 0 j)
  (< j ($Seq.length s0))) (= ($Seq.index s0 j) ($Seq.index s1 j)))
  :pattern ( ($Seq.index s0 j))
  :pattern ( ($Seq.index s1 j))
  ))))
  (=> (and
  (= ($Seq.length s0) ($Seq.length s1))
  (forall ((j Int) ) (! (=> (and
  (<= 0 j)
  (< j ($Seq.length s0))) (= ($Seq.index s0 j) ($Seq.index s1 j)))
  :pattern ( ($Seq.index s0 j))
  :pattern ( ($Seq.index s1 j))
  ))) ($Seq.equal s0 s1)))
  :pattern ( ($Seq.equal s0 s1))
  )))
(assert (forall ((a $Seq<$Ref>) (b $Seq<$Ref>) ) (! (=> ($Seq.equal a b) (= a b))
  :pattern ( ($Seq.equal a b))
  )))
(assert (forall ((s0 $Seq<$Ref>) (s1 $Seq<$Ref>) (n Int) ) (! (and
  (=> ($Seq.sameuntil s0 s1 n) (forall ((j Int) ) (! (=> (and
  (<= 0 j)
  (< j n)) (= ($Seq.index s0 j) ($Seq.index s1 j)))
  :pattern ( ($Seq.index s0 j))
  :pattern ( ($Seq.index s1 j))
  )))
  (=> (forall ((j Int) ) (! (=> (and
  (<= 0 j)
  (< j n)) (= ($Seq.index s0 j) ($Seq.index s1 j)))
  :pattern ( ($Seq.index s0 j))
  :pattern ( ($Seq.index s1 j))
  )) ($Seq.sameuntil s0 s1 n)))
  :pattern ( ($Seq.sameuntil s0 s1 n))
  )))
(assert (forall ((s $Seq<$Ref>) (n Int) ) (! (=> (<= 0 n) (and
  (=> (<= n ($Seq.length s)) (= ($Seq.length ($Seq.take s n)) n))
  (=> (< ($Seq.length s) n) (= ($Seq.length ($Seq.take s n)) ($Seq.length s)))))
  :pattern ( ($Seq.length ($Seq.take s n)))
  )))
(assert (forall ((s $Seq<$Ref>) (n Int) (j Int) ) (! (=> (and
  (<= 0 j)
  (< j n)
  (< j ($Seq.length s))) (= ($Seq.index ($Seq.take s n) j) ($Seq.index s j)))
  :pattern ( ($Seq.index ($Seq.take s n) j))
  )))
(assert (forall ((s $Seq<$Ref>) (n Int) ) (! (=> (<= 0 n) (and
  (=> (<= n ($Seq.length s)) (= ($Seq.length ($Seq.drop s n)) (- ($Seq.length s) n)))
  (=> (< ($Seq.length s) n) (= ($Seq.length ($Seq.drop s n)) 0))))
  :pattern ( ($Seq.length ($Seq.drop s n)))
  )))
(assert (forall ((s $Seq<$Ref>) (n Int) (j Int) ) (! (=> (and
  (<= 0 n)
  (<= 0 j)
  (< j (- ($Seq.length s) n))) (= ($Seq.index ($Seq.drop s n) j) ($Seq.index s (+ j n))))
  :pattern ( ($Seq.index ($Seq.drop s n) j))
  )))
(assert (forall ((s $Seq<$Ref>) (i Int) (v $Ref) (n Int) ) (! (=> (and
  (<= 0 i)
  (< i n)
  (<= n ($Seq.length s))) (= ($Seq.take ($Seq.update s i v) n) ($Seq.update ($Seq.take s n) i v)))
  :pattern ( ($Seq.take ($Seq.update s i v) n))
  )))
(assert (forall ((s $Seq<$Ref>) (i Int) (v $Ref) (n Int) ) (! (=> (and
  (<= n i)
  (< i ($Seq.length s))) (= ($Seq.take ($Seq.update s i v) n) ($Seq.take s n)))
  :pattern ( ($Seq.take ($Seq.update s i v) n))
  )))
(assert (forall ((s $Seq<$Ref>) (i Int) (v $Ref) (n Int) ) (! (=> (and
  (<= 0 n)
  (<= n i)
  (< i ($Seq.length s))) (= ($Seq.drop ($Seq.update s i v) n) ($Seq.update ($Seq.drop s n) (- i n) v)))
  :pattern ( ($Seq.drop ($Seq.update s i v) n))
  )))
(assert (forall ((s $Seq<$Ref>) (i Int) (v $Ref) (n Int) ) (! (=> (and
  (<= 0 i)
  (< i n)
  (< n ($Seq.length s))) (= ($Seq.drop ($Seq.update s i v) n) ($Seq.drop s n)))
  :pattern ( ($Seq.drop ($Seq.update s i v) n))
  )))
(assert (forall ((s $Seq<$Ref>) (v $Ref) (n Int) ) (! (=> (and
  (<= 0 n)
  (<= n ($Seq.length s))) (= ($Seq.drop ($Seq.build s v) n) ($Seq.build ($Seq.drop s n) v)))
  :pattern ( ($Seq.drop ($Seq.build s v) n))
  )))
(assert (forall ((s $Seq<$Ref>) (n Int) ) (! (=> (= n 0) (= ($Seq.drop s n) s))
  :pattern ( ($Seq.drop s n))
  )))
(assert (forall ((s $Seq<$Ref>) (n Int) ) (! (=> (= n 0) (= ($Seq.take s n) $Seq.empty<$Ref>))
  :pattern ( ($Seq.take s n))
  )))
(assert (forall ((s $Seq<$Ref>) (m Int) (n Int) ) (! (=> (and
  (<= 0 m)
  (<= 0 n)
  (<= (+ m n) ($Seq.length s))) (= ($Seq.drop ($Seq.drop s m) n) ($Seq.drop s (+ m n))))
  :pattern ( ($Seq.drop ($Seq.drop s m) n))
  )))
(assert (forall ((x $Ref) (y $Ref)) (!
  (iff
    ($Seq.contains ($Seq.singleton x) y)
    (= x y))
  :pattern (($Seq.contains ($Seq.singleton x) y))
  )))
; /dafny_axioms/sequences_axioms_dafny.smt2 [Int]
(assert (forall ((s $Seq<Int>) ) (! (<= 0 ($Seq.length s))
  :pattern ( ($Seq.length s))
  )))
(assert (= ($Seq.length $Seq.empty<Int>) 0))
(assert (forall ((s $Seq<Int>) ) (! (=> (= ($Seq.length s) 0) (= s $Seq.empty<Int>))
  :pattern ( ($Seq.length s))
  )))
(assert (forall ((t Int) ) (! (= ($Seq.length ($Seq.singleton t)) 1)
  :pattern ( ($Seq.length ($Seq.singleton t)))
  )))
(assert (forall ((s $Seq<Int>) (v Int) ) (! (= ($Seq.length ($Seq.build s v)) (+ 1 ($Seq.length s)))
  :pattern ( ($Seq.length ($Seq.build s v)))
  )))
(assert (forall ((s $Seq<Int>) (i Int) (v Int) ) (! (and
  (=> (= i ($Seq.length s)) (= ($Seq.index ($Seq.build s v) i) v))
  (=> (not (= i ($Seq.length s))) (= ($Seq.index ($Seq.build s v) i) ($Seq.index s i))))
  :pattern ( ($Seq.index ($Seq.build s v) i))
  )))
(assert (forall ((s0 $Seq<Int>) (s1 $Seq<Int>) ) (! (= ($Seq.length ($Seq.append s0 s1)) (+ ($Seq.length s0) ($Seq.length s1)))
  :pattern ( ($Seq.length ($Seq.append s0 s1)))
  )))
(assert (forall ((t Int) ) (! (= ($Seq.index ($Seq.singleton t) 0) t)
  :pattern ( ($Seq.index ($Seq.singleton t) 0))
  )))
(assert (forall ((s0 $Seq<Int>) (s1 $Seq<Int>) (n Int) ) (! (and
  (=> (< n ($Seq.length s0)) (= ($Seq.index ($Seq.append s0 s1) n) ($Seq.index s0 n)))
  (=> (<= ($Seq.length s0) n) (= ($Seq.index ($Seq.append s0 s1) n) ($Seq.index s1 (- n ($Seq.length s0))))))
  :pattern ( ($Seq.index ($Seq.append s0 s1) n))
  )))
(assert (forall ((s $Seq<Int>) (i Int) (v Int) ) (! (=> (and
  (<= 0 i)
  (< i ($Seq.length s))) (= ($Seq.length ($Seq.update s i v)) ($Seq.length s)))
  :pattern ( ($Seq.length ($Seq.update s i v)))
  )))
(assert (forall ((s $Seq<Int>) (i Int) (v Int) (n Int) ) (! (=> (and
  (<= 0 n)
  (< n ($Seq.length s))) (and
  (=> (= i n) (= ($Seq.index ($Seq.update s i v) n) v))
  (=> (not (= i n)) (= ($Seq.index ($Seq.update s i v) n) ($Seq.index s n)))))
  :pattern ( ($Seq.index ($Seq.update s i v) n))
  )))
(assert (forall ((s $Seq<Int>) (x Int) ) (! (and
  (=> ($Seq.contains s x) (exists ((i Int) ) (! (and
  (<= 0 i)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )))
  (=> (exists ((i Int) ) (! (and
  (<= 0 i)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )) ($Seq.contains s x)))
  :pattern ( ($Seq.contains s x))
  )))
(assert (forall ((x Int) ) (! (not ($Seq.contains $Seq.empty<Int> x))
  :pattern ( ($Seq.contains $Seq.empty<Int> x))
  )))
(assert (forall ((s0 $Seq<Int>) (s1 $Seq<Int>) (x Int) ) (! (and
  (=> ($Seq.contains ($Seq.append s0 s1) x) (or
  ($Seq.contains s0 x)
  ($Seq.contains s1 x)))
  (=> (or
  ($Seq.contains s0 x)
  ($Seq.contains s1 x)) ($Seq.contains ($Seq.append s0 s1) x)))
  :pattern ( ($Seq.contains ($Seq.append s0 s1) x))
  )))
(assert (forall ((s $Seq<Int>) (v Int) (x Int) ) (! (and
  (=> ($Seq.contains ($Seq.build s v) x) (or
  (= v x)
  ($Seq.contains s x)))
  (=> (or
  (= v x)
  ($Seq.contains s x)) ($Seq.contains ($Seq.build s v) x)))
  :pattern ( ($Seq.contains ($Seq.build s v) x))
  )))
(assert (forall ((s $Seq<Int>) (n Int) (x Int) ) (! (and
  (=> ($Seq.contains ($Seq.take s n) x) (exists ((i Int) ) (! (and
  (<= 0 i)
  (< i n)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )))
  (=> (exists ((i Int) ) (! (and
  (<= 0 i)
  (< i n)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )) ($Seq.contains ($Seq.take s n) x)))
  :pattern ( ($Seq.contains ($Seq.take s n) x))
  )))
(assert (forall ((s $Seq<Int>) (n Int) (x Int) ) (! (and
  (=> ($Seq.contains ($Seq.drop s n) x) (exists ((i Int) ) (! (and
  (<= 0 n)
  (<= n i)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )))
  (=> (exists ((i Int) ) (! (and
  (<= 0 n)
  (<= n i)
  (< i ($Seq.length s))
  (= ($Seq.index s i) x))
  :pattern ( ($Seq.index s i))
  )) ($Seq.contains ($Seq.drop s n) x)))
  :pattern ( ($Seq.contains ($Seq.drop s n) x))
  )))
(assert (forall ((s0 $Seq<Int>) (s1 $Seq<Int>) ) (! (and
  (=> ($Seq.equal s0 s1) (and
  (= ($Seq.length s0) ($Seq.length s1))
  (forall ((j Int) ) (! (=> (and
  (<= 0 j)
  (< j ($Seq.length s0))) (= ($Seq.index s0 j) ($Seq.index s1 j)))
  :pattern ( ($Seq.index s0 j))
  :pattern ( ($Seq.index s1 j))
  ))))
  (=> (and
  (= ($Seq.length s0) ($Seq.length s1))
  (forall ((j Int) ) (! (=> (and
  (<= 0 j)
  (< j ($Seq.length s0))) (= ($Seq.index s0 j) ($Seq.index s1 j)))
  :pattern ( ($Seq.index s0 j))
  :pattern ( ($Seq.index s1 j))
  ))) ($Seq.equal s0 s1)))
  :pattern ( ($Seq.equal s0 s1))
  )))
(assert (forall ((a $Seq<Int>) (b $Seq<Int>) ) (! (=> ($Seq.equal a b) (= a b))
  :pattern ( ($Seq.equal a b))
  )))
(assert (forall ((s0 $Seq<Int>) (s1 $Seq<Int>) (n Int) ) (! (and
  (=> ($Seq.sameuntil s0 s1 n) (forall ((j Int) ) (! (=> (and
  (<= 0 j)
  (< j n)) (= ($Seq.index s0 j) ($Seq.index s1 j)))
  :pattern ( ($Seq.index s0 j))
  :pattern ( ($Seq.index s1 j))
  )))
  (=> (forall ((j Int) ) (! (=> (and
  (<= 0 j)
  (< j n)) (= ($Seq.index s0 j) ($Seq.index s1 j)))
  :pattern ( ($Seq.index s0 j))
  :pattern ( ($Seq.index s1 j))
  )) ($Seq.sameuntil s0 s1 n)))
  :pattern ( ($Seq.sameuntil s0 s1 n))
  )))
(assert (forall ((s $Seq<Int>) (n Int) ) (! (=> (<= 0 n) (and
  (=> (<= n ($Seq.length s)) (= ($Seq.length ($Seq.take s n)) n))
  (=> (< ($Seq.length s) n) (= ($Seq.length ($Seq.take s n)) ($Seq.length s)))))
  :pattern ( ($Seq.length ($Seq.take s n)))
  )))
(assert (forall ((s $Seq<Int>) (n Int) (j Int) ) (! (=> (and
  (<= 0 j)
  (< j n)
  (< j ($Seq.length s))) (= ($Seq.index ($Seq.take s n) j) ($Seq.index s j)))
  :pattern ( ($Seq.index ($Seq.take s n) j))
  )))
(assert (forall ((s $Seq<Int>) (n Int) ) (! (=> (<= 0 n) (and
  (=> (<= n ($Seq.length s)) (= ($Seq.length ($Seq.drop s n)) (- ($Seq.length s) n)))
  (=> (< ($Seq.length s) n) (= ($Seq.length ($Seq.drop s n)) 0))))
  :pattern ( ($Seq.length ($Seq.drop s n)))
  )))
(assert (forall ((s $Seq<Int>) (n Int) (j Int) ) (! (=> (and
  (<= 0 n)
  (<= 0 j)
  (< j (- ($Seq.length s) n))) (= ($Seq.index ($Seq.drop s n) j) ($Seq.index s (+ j n))))
  :pattern ( ($Seq.index ($Seq.drop s n) j))
  )))
(assert (forall ((s $Seq<Int>) (i Int) (v Int) (n Int) ) (! (=> (and
  (<= 0 i)
  (< i n)
  (<= n ($Seq.length s))) (= ($Seq.take ($Seq.update s i v) n) ($Seq.update ($Seq.take s n) i v)))
  :pattern ( ($Seq.take ($Seq.update s i v) n))
  )))
(assert (forall ((s $Seq<Int>) (i Int) (v Int) (n Int) ) (! (=> (and
  (<= n i)
  (< i ($Seq.length s))) (= ($Seq.take ($Seq.update s i v) n) ($Seq.take s n)))
  :pattern ( ($Seq.take ($Seq.update s i v) n))
  )))
(assert (forall ((s $Seq<Int>) (i Int) (v Int) (n Int) ) (! (=> (and
  (<= 0 n)
  (<= n i)
  (< i ($Seq.length s))) (= ($Seq.drop ($Seq.update s i v) n) ($Seq.update ($Seq.drop s n) (- i n) v)))
  :pattern ( ($Seq.drop ($Seq.update s i v) n))
  )))
(assert (forall ((s $Seq<Int>) (i Int) (v Int) (n Int) ) (! (=> (and
  (<= 0 i)
  (< i n)
  (< n ($Seq.length s))) (= ($Seq.drop ($Seq.update s i v) n) ($Seq.drop s n)))
  :pattern ( ($Seq.drop ($Seq.update s i v) n))
  )))
(assert (forall ((s $Seq<Int>) (v Int) (n Int) ) (! (=> (and
  (<= 0 n)
  (<= n ($Seq.length s))) (= ($Seq.drop ($Seq.build s v) n) ($Seq.build ($Seq.drop s n) v)))
  :pattern ( ($Seq.drop ($Seq.build s v) n))
  )))
(assert (forall ((s $Seq<Int>) (n Int) ) (! (=> (= n 0) (= ($Seq.drop s n) s))
  :pattern ( ($Seq.drop s n))
  )))
(assert (forall ((s $Seq<Int>) (n Int) ) (! (=> (= n 0) (= ($Seq.take s n) $Seq.empty<Int>))
  :pattern ( ($Seq.take s n))
  )))
(assert (forall ((s $Seq<Int>) (m Int) (n Int) ) (! (=> (and
  (<= 0 m)
  (<= 0 n)
  (<= (+ m n) ($Seq.length s))) (= ($Seq.drop ($Seq.drop s m) n) ($Seq.drop s (+ m n))))
  :pattern ( ($Seq.drop ($Seq.drop s m) n))
  )))
(assert (forall ((x Int) (y Int)) (!
  (iff
    ($Seq.contains ($Seq.singleton x) y)
    (= x y))
  :pattern (($Seq.contains ($Seq.singleton x) y))
  )))
; /dafny_axioms/sequences_int_axioms_dafny.smt2
(assert (forall ((min Int) (max Int) ) (! (and
  (=> (< min max) (= ($Seq.length ($Seq.range min max)) (- max min)))
  (=> (<= max min) (= ($Seq.length ($Seq.range min max)) 0)))
   :pattern ( ($Seq.length ($Seq.range min max)))
  )))
(assert (forall ((min Int) (max Int) (j Int) ) (! (=> (and
  (<= 0 j)
  (< j (- max min))) (= ($Seq.index ($Seq.range min max) j) (+ min j)))
   :pattern ( ($Seq.index ($Seq.range min max) j))
  )))
(assert (forall ((min Int) (max Int) (v Int) ) (! (and
  (=> ($Seq.contains ($Seq.range min max) v) (and
  (<= min v)
  (< v max)))
  (=> (and
  (<= min v)
  (< v max)) ($Seq.contains ($Seq.range min max) v)))
   :pattern ( ($Seq.contains ($Seq.range min max) v))
  )))
; /dafny_axioms/sets_axioms_dafny.smt2 [Seq[Ref]]
(assert (forall ((s $Set<$Seq<$Ref>>)) (!
  (<= 0 ($Set.card s))
  :pattern (($Set.card s))
  )))
(assert (forall ((o $Seq<$Ref>)) (!
  (not ($Set.in o $Set.empty<$Seq<$Ref>>))
  :pattern (($Set.in o $Set.empty<$Seq<$Ref>>))
  )))
(assert (forall ((s $Set<$Seq<$Ref>>)) (!
  (and
    (iff
      (= ($Set.card s) 0)
      (= s $Set.empty<$Seq<$Ref>>))
    (implies
      (not (= ($Set.card s) 0))
      (exists ((x $Seq<$Ref>)) (!
        ($Set.in x s)
        :pattern (($Set.in x s))
      ))))
  :pattern (($Set.card s))
  )))
(assert (forall ((r $Seq<$Ref>)) (!
  ($Set.in r ($Set.singleton r))
  :pattern (($Set.in r ($Set.singleton r)))
  )))
(assert (forall ((r $Seq<$Ref>) (o $Seq<$Ref>)) (!
  (iff
    ($Set.in o ($Set.singleton r))
    (= r o))
  :pattern (($Set.in o ($Set.singleton r)))
  )))
(assert (forall ((r $Seq<$Ref>)) (!
  (= ($Set.card ($Set.singleton r)) 1)
  :pattern (($Set.card ($Set.singleton r)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (x $Seq<$Ref>) (o $Seq<$Ref>)) (!
  (iff
    ($Set.in o ($Set.unionone a x))
    (or
      (= o x)
      ($Set.in o a)))
  :pattern (($Set.in o ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (x $Seq<$Ref>)) (!
  ($Set.in x ($Set.unionone a x))
  :pattern (($Set.in x ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (x $Seq<$Ref>) (y $Seq<$Ref>)) (!
  (=>
    ($Set.in y a)
    ($Set.in y ($Set.unionone a x)))
  :pattern (($Set.in y a) ($Set.in y ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (x $Seq<$Ref>)) (!
  (=>
    ($Set.in x a)
    (= ($Set.card ($Set.unionone a x)) ($Set.card a)))
  :pattern (($Set.card ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (x $Seq<$Ref>)) (!
  (=>
    (not ($Set.in x a))
    (= ($Set.card ($Set.unionone a x)) (+ ($Set.card a) 1)))
  :pattern (($Set.card ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>) (o $Seq<$Ref>)) (!
  (iff
    ($Set.in o ($Set.union a b))
    (or
      ($Set.in o a)
      ($Set.in o b)))
  :pattern (($Set.in o ($Set.union a b)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>) (y $Seq<$Ref>)) (!
  (=>
    ($Set.in y a)
    ($Set.in y ($Set.union a b)))
  :pattern (($Set.in y ($Set.union a b)) ($Set.in y a))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>) (y $Seq<$Ref>)) (!
  (=>
    ($Set.in y b)
    ($Set.in y ($Set.union a b)))
  :pattern (($Set.in y ($Set.union a b)) ($Set.in y b))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>) (o $Seq<$Ref>)) (!
  (iff
    ($Set.in o ($Set.intersection a b))
    (and
      ($Set.in o a)
      ($Set.in o b)))
  :pattern (($Set.in o ($Set.intersection a b)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>)) (!
  (=
    ($Set.union ($Set.union a b) b)
    ($Set.union a b))
  :pattern (($Set.union ($Set.union a b) b))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>)) (!
  (=
    ($Set.union a ($Set.union a b))
    ($Set.union a b))
    :pattern (($Set.union a ($Set.union a b)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>)) (!
  (=
    ($Set.intersection ($Set.intersection a b) b)
    ($Set.intersection a b))
  :pattern (($Set.intersection ($Set.intersection a b) b))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>)) (!
  (=
    ($Set.intersection a ($Set.intersection a b))
    ($Set.intersection a b))
  :pattern (($Set.intersection a ($Set.intersection a b)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>)) (!
  (=
    (+
      ($Set.card ($Set.union a b))
      ($Set.card ($Set.intersection a b)))
    (+
      ($Set.card a)
      ($Set.card b)))
  :pattern (($Set.card ($Set.union a b)))
  :pattern (($Set.card ($Set.intersection a b)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>) (o $Seq<$Ref>)) (!
  (iff
    ($Set.in o ($Set.difference a b))
    (and
      ($Set.in o a)
      (not ($Set.in o b))))
  :pattern (($Set.in o ($Set.difference a b)))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>) (y $Seq<$Ref>)) (!
  (=>
    ($Set.in y b)
    (not ($Set.in y ($Set.difference a b))))
  :pattern (($Set.in y ($Set.difference a b)) ($Set.in y b))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>)) (!
  (iff
    ($Set.subset a b)
    (forall ((o $Seq<$Ref>)) (!
      (=>
        ($Set.in o a)
        ($Set.in o b))
      :pattern (($Set.in o a))
      :pattern (($Set.in o b))
    )))
  :pattern (($Set.subset a b))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>)) (!
  (iff
    ($Set.equal a b)
    (forall ((o $Seq<$Ref>)) (!
      (iff
        ($Set.in o a)
        ($Set.in o b))
      :pattern (($Set.in o a))
      :pattern (($Set.in o b))
      )))
  :pattern (($Set.equal a b))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>)) (!
  (=>
    ($Set.equal a b)
    (= a b))
  :pattern (($Set.equal a b))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>)) (!
  (iff
    ($Set.disjoint a b)
    (forall ((o $Seq<$Ref>)) (!
      (or
        (not ($Set.in o a))
        (not ($Set.in o b)))
      :pattern (($Set.in o a))
      :pattern (($Set.in o b))
      )))
  :pattern (($Set.disjoint a b))
  )))
(assert (forall ((a $Set<$Seq<$Ref>>) (b $Set<$Seq<$Ref>>)) (!
  (and
    (=
      (+
        (+
          ($Set.card ($Set.difference a b))
          ($Set.card ($Set.difference b a)))
        ($Set.card ($Set.intersection a b)))
      ($Set.card ($Set.union a b)))
    (=
      ($Set.card ($Set.difference a b))
      (-
        ($Set.card a)
        ($Set.card ($Set.intersection a b)))))
  :pattern (($Set.card ($Set.difference a b)) ($Set.card ($Set.intersection a b)))
  )))
; /dafny_axioms/sets_axioms_dafny.smt2 [Int]
(assert (forall ((s $Set<Int>)) (!
  (<= 0 ($Set.card s))
  :pattern (($Set.card s))
  )))
(assert (forall ((o Int)) (!
  (not ($Set.in o $Set.empty<Int>))
  :pattern (($Set.in o $Set.empty<Int>))
  )))
(assert (forall ((s $Set<Int>)) (!
  (and
    (iff
      (= ($Set.card s) 0)
      (= s $Set.empty<Int>))
    (implies
      (not (= ($Set.card s) 0))
      (exists ((x Int)) (!
        ($Set.in x s)
        :pattern (($Set.in x s))
      ))))
  :pattern (($Set.card s))
  )))
(assert (forall ((r Int)) (!
  ($Set.in r ($Set.singleton r))
  :pattern (($Set.in r ($Set.singleton r)))
  )))
(assert (forall ((r Int) (o Int)) (!
  (iff
    ($Set.in o ($Set.singleton r))
    (= r o))
  :pattern (($Set.in o ($Set.singleton r)))
  )))
(assert (forall ((r Int)) (!
  (= ($Set.card ($Set.singleton r)) 1)
  :pattern (($Set.card ($Set.singleton r)))
  )))
(assert (forall ((a $Set<Int>) (x Int) (o Int)) (!
  (iff
    ($Set.in o ($Set.unionone a x))
    (or
      (= o x)
      ($Set.in o a)))
  :pattern (($Set.in o ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<Int>) (x Int)) (!
  ($Set.in x ($Set.unionone a x))
  :pattern (($Set.in x ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<Int>) (x Int) (y Int)) (!
  (=>
    ($Set.in y a)
    ($Set.in y ($Set.unionone a x)))
  :pattern (($Set.in y a) ($Set.in y ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<Int>) (x Int)) (!
  (=>
    ($Set.in x a)
    (= ($Set.card ($Set.unionone a x)) ($Set.card a)))
  :pattern (($Set.card ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<Int>) (x Int)) (!
  (=>
    (not ($Set.in x a))
    (= ($Set.card ($Set.unionone a x)) (+ ($Set.card a) 1)))
  :pattern (($Set.card ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>) (o Int)) (!
  (iff
    ($Set.in o ($Set.union a b))
    (or
      ($Set.in o a)
      ($Set.in o b)))
  :pattern (($Set.in o ($Set.union a b)))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>) (y Int)) (!
  (=>
    ($Set.in y a)
    ($Set.in y ($Set.union a b)))
  :pattern (($Set.in y ($Set.union a b)) ($Set.in y a))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>) (y Int)) (!
  (=>
    ($Set.in y b)
    ($Set.in y ($Set.union a b)))
  :pattern (($Set.in y ($Set.union a b)) ($Set.in y b))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>) (o Int)) (!
  (iff
    ($Set.in o ($Set.intersection a b))
    (and
      ($Set.in o a)
      ($Set.in o b)))
  :pattern (($Set.in o ($Set.intersection a b)))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>)) (!
  (=
    ($Set.union ($Set.union a b) b)
    ($Set.union a b))
  :pattern (($Set.union ($Set.union a b) b))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>)) (!
  (=
    ($Set.union a ($Set.union a b))
    ($Set.union a b))
    :pattern (($Set.union a ($Set.union a b)))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>)) (!
  (=
    ($Set.intersection ($Set.intersection a b) b)
    ($Set.intersection a b))
  :pattern (($Set.intersection ($Set.intersection a b) b))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>)) (!
  (=
    ($Set.intersection a ($Set.intersection a b))
    ($Set.intersection a b))
  :pattern (($Set.intersection a ($Set.intersection a b)))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>)) (!
  (=
    (+
      ($Set.card ($Set.union a b))
      ($Set.card ($Set.intersection a b)))
    (+
      ($Set.card a)
      ($Set.card b)))
  :pattern (($Set.card ($Set.union a b)))
  :pattern (($Set.card ($Set.intersection a b)))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>) (o Int)) (!
  (iff
    ($Set.in o ($Set.difference a b))
    (and
      ($Set.in o a)
      (not ($Set.in o b))))
  :pattern (($Set.in o ($Set.difference a b)))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>) (y Int)) (!
  (=>
    ($Set.in y b)
    (not ($Set.in y ($Set.difference a b))))
  :pattern (($Set.in y ($Set.difference a b)) ($Set.in y b))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>)) (!
  (iff
    ($Set.subset a b)
    (forall ((o Int)) (!
      (=>
        ($Set.in o a)
        ($Set.in o b))
      :pattern (($Set.in o a))
      :pattern (($Set.in o b))
    )))
  :pattern (($Set.subset a b))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>)) (!
  (iff
    ($Set.equal a b)
    (forall ((o Int)) (!
      (iff
        ($Set.in o a)
        ($Set.in o b))
      :pattern (($Set.in o a))
      :pattern (($Set.in o b))
      )))
  :pattern (($Set.equal a b))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>)) (!
  (=>
    ($Set.equal a b)
    (= a b))
  :pattern (($Set.equal a b))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>)) (!
  (iff
    ($Set.disjoint a b)
    (forall ((o Int)) (!
      (or
        (not ($Set.in o a))
        (not ($Set.in o b)))
      :pattern (($Set.in o a))
      :pattern (($Set.in o b))
      )))
  :pattern (($Set.disjoint a b))
  )))
(assert (forall ((a $Set<Int>) (b $Set<Int>)) (!
  (and
    (=
      (+
        (+
          ($Set.card ($Set.difference a b))
          ($Set.card ($Set.difference b a)))
        ($Set.card ($Set.intersection a b)))
      ($Set.card ($Set.union a b)))
    (=
      ($Set.card ($Set.difference a b))
      (-
        ($Set.card a)
        ($Set.card ($Set.intersection a b)))))
  :pattern (($Set.card ($Set.difference a b)) ($Set.card ($Set.intersection a b)))
  )))
; /dafny_axioms/sets_axioms_dafny.smt2 [Ref]
(assert (forall ((s $Set<$Ref>)) (!
  (<= 0 ($Set.card s))
  :pattern (($Set.card s))
  )))
(assert (forall ((o $Ref)) (!
  (not ($Set.in o $Set.empty<$Ref>))
  :pattern (($Set.in o $Set.empty<$Ref>))
  )))
(assert (forall ((s $Set<$Ref>)) (!
  (and
    (iff
      (= ($Set.card s) 0)
      (= s $Set.empty<$Ref>))
    (implies
      (not (= ($Set.card s) 0))
      (exists ((x $Ref)) (!
        ($Set.in x s)
        :pattern (($Set.in x s))
      ))))
  :pattern (($Set.card s))
  )))
(assert (forall ((r $Ref)) (!
  ($Set.in r ($Set.singleton r))
  :pattern (($Set.in r ($Set.singleton r)))
  )))
(assert (forall ((r $Ref) (o $Ref)) (!
  (iff
    ($Set.in o ($Set.singleton r))
    (= r o))
  :pattern (($Set.in o ($Set.singleton r)))
  )))
(assert (forall ((r $Ref)) (!
  (= ($Set.card ($Set.singleton r)) 1)
  :pattern (($Set.card ($Set.singleton r)))
  )))
(assert (forall ((a $Set<$Ref>) (x $Ref) (o $Ref)) (!
  (iff
    ($Set.in o ($Set.unionone a x))
    (or
      (= o x)
      ($Set.in o a)))
  :pattern (($Set.in o ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<$Ref>) (x $Ref)) (!
  ($Set.in x ($Set.unionone a x))
  :pattern (($Set.in x ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<$Ref>) (x $Ref) (y $Ref)) (!
  (=>
    ($Set.in y a)
    ($Set.in y ($Set.unionone a x)))
  :pattern (($Set.in y a) ($Set.in y ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<$Ref>) (x $Ref)) (!
  (=>
    ($Set.in x a)
    (= ($Set.card ($Set.unionone a x)) ($Set.card a)))
  :pattern (($Set.card ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<$Ref>) (x $Ref)) (!
  (=>
    (not ($Set.in x a))
    (= ($Set.card ($Set.unionone a x)) (+ ($Set.card a) 1)))
  :pattern (($Set.card ($Set.unionone a x)))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>) (o $Ref)) (!
  (iff
    ($Set.in o ($Set.union a b))
    (or
      ($Set.in o a)
      ($Set.in o b)))
  :pattern (($Set.in o ($Set.union a b)))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>) (y $Ref)) (!
  (=>
    ($Set.in y a)
    ($Set.in y ($Set.union a b)))
  :pattern (($Set.in y ($Set.union a b)) ($Set.in y a))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>) (y $Ref)) (!
  (=>
    ($Set.in y b)
    ($Set.in y ($Set.union a b)))
  :pattern (($Set.in y ($Set.union a b)) ($Set.in y b))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>) (o $Ref)) (!
  (iff
    ($Set.in o ($Set.intersection a b))
    (and
      ($Set.in o a)
      ($Set.in o b)))
  :pattern (($Set.in o ($Set.intersection a b)))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>)) (!
  (=
    ($Set.union ($Set.union a b) b)
    ($Set.union a b))
  :pattern (($Set.union ($Set.union a b) b))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>)) (!
  (=
    ($Set.union a ($Set.union a b))
    ($Set.union a b))
    :pattern (($Set.union a ($Set.union a b)))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>)) (!
  (=
    ($Set.intersection ($Set.intersection a b) b)
    ($Set.intersection a b))
  :pattern (($Set.intersection ($Set.intersection a b) b))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>)) (!
  (=
    ($Set.intersection a ($Set.intersection a b))
    ($Set.intersection a b))
  :pattern (($Set.intersection a ($Set.intersection a b)))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>)) (!
  (=
    (+
      ($Set.card ($Set.union a b))
      ($Set.card ($Set.intersection a b)))
    (+
      ($Set.card a)
      ($Set.card b)))
  :pattern (($Set.card ($Set.union a b)))
  :pattern (($Set.card ($Set.intersection a b)))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>) (o $Ref)) (!
  (iff
    ($Set.in o ($Set.difference a b))
    (and
      ($Set.in o a)
      (not ($Set.in o b))))
  :pattern (($Set.in o ($Set.difference a b)))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>) (y $Ref)) (!
  (=>
    ($Set.in y b)
    (not ($Set.in y ($Set.difference a b))))
  :pattern (($Set.in y ($Set.difference a b)) ($Set.in y b))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>)) (!
  (iff
    ($Set.subset a b)
    (forall ((o $Ref)) (!
      (=>
        ($Set.in o a)
        ($Set.in o b))
      :pattern (($Set.in o a))
      :pattern (($Set.in o b))
    )))
  :pattern (($Set.subset a b))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>)) (!
  (iff
    ($Set.equal a b)
    (forall ((o $Ref)) (!
      (iff
        ($Set.in o a)
        ($Set.in o b))
      :pattern (($Set.in o a))
      :pattern (($Set.in o b))
      )))
  :pattern (($Set.equal a b))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>)) (!
  (=>
    ($Set.equal a b)
    (= a b))
  :pattern (($Set.equal a b))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>)) (!
  (iff
    ($Set.disjoint a b)
    (forall ((o $Ref)) (!
      (or
        (not ($Set.in o a))
        (not ($Set.in o b)))
      :pattern (($Set.in o a))
      :pattern (($Set.in o b))
      )))
  :pattern (($Set.disjoint a b))
  )))
(assert (forall ((a $Set<$Ref>) (b $Set<$Ref>)) (!
  (and
    (=
      (+
        (+
          ($Set.card ($Set.difference a b))
          ($Set.card ($Set.difference b a)))
        ($Set.card ($Set.intersection a b)))
      ($Set.card ($Set.union a b)))
    (=
      ($Set.card ($Set.difference a b))
      (-
        ($Set.card a)
        ($Set.card ($Set.intersection a b)))))
  :pattern (($Set.card ($Set.difference a b)) ($Set.card ($Set.intersection a b)))
  )))
; /field_value_functions_axioms.smt2 [dst: Seq[Ref]]
(assert (forall ((vs $FVF<$Seq<$Ref>>) (ws $FVF<$Seq<$Ref>>)) (!
    (implies
      (and
        ($Set.equal ($FVF.domain_dst vs) ($FVF.domain_dst ws))
        (forall ((x $Ref)) (!
          (implies
            ($Set.in x ($FVF.domain_dst vs))
            (= ($FVF.lookup_dst vs x) ($FVF.lookup_dst ws x)))
          :pattern (($FVF.lookup_dst vs x) ($FVF.lookup_dst ws x)))))
      (= vs ws))
    :pattern (($FVF.domain_dst vs) ($FVF.domain_dst ws)))))
; /field_value_functions_axioms.smt2 [src: Seq[Ref]]
(assert (forall ((vs $FVF<$Seq<$Ref>>) (ws $FVF<$Seq<$Ref>>)) (!
    (implies
      (and
        ($Set.equal ($FVF.domain_src vs) ($FVF.domain_src ws))
        (forall ((x $Ref)) (!
          (implies
            ($Set.in x ($FVF.domain_src vs))
            (= ($FVF.lookup_src vs x) ($FVF.lookup_src ws x)))
          :pattern (($FVF.lookup_src vs x) ($FVF.lookup_src ws x)))))
      (= vs ws))
    :pattern (($FVF.domain_src vs) ($FVF.domain_src ws)))))
; /field_value_functions_axioms.smt2 [Integer_value: Int]
(assert (forall ((vs $FVF<Int>) (ws $FVF<Int>)) (!
    (implies
      (and
        ($Set.equal ($FVF.domain_Integer_value vs) ($FVF.domain_Integer_value ws))
        (forall ((x $Ref)) (!
          (implies
            ($Set.in x ($FVF.domain_Integer_value vs))
            (= ($FVF.lookup_Integer_value vs x) ($FVF.lookup_Integer_value ws x)))
          :pattern (($FVF.lookup_Integer_value vs x) ($FVF.lookup_Integer_value ws x)))))
      (= vs ws))
    :pattern (($FVF.domain_Integer_value vs) ($FVF.domain_Integer_value ws)))))
; Declaring additional sort wrappers
(declare-fun $SortWrappers.$PermTo$Snap ($Perm) $Snap)
(declare-fun $SortWrappers.$SnapTo$Perm ($Snap) $Perm)
(assert (forall ((x $Perm)) (!
    (= x ($SortWrappers.$SnapTo$Perm($SortWrappers.$PermTo$Snap x)))
    :pattern (($SortWrappers.$PermTo$Snap x))
    )))
(declare-fun $SortWrappers.$RefTo$Snap ($Ref) $Snap)
(declare-fun $SortWrappers.$SnapTo$Ref ($Snap) $Ref)
(assert (forall ((x $Ref)) (!
    (= x ($SortWrappers.$SnapTo$Ref($SortWrappers.$RefTo$Snap x)))
    :pattern (($SortWrappers.$RefTo$Snap x))
    )))
(declare-fun $SortWrappers.BoolTo$Snap (Bool) $Snap)
(declare-fun $SortWrappers.$SnapToBool ($Snap) Bool)
(assert (forall ((x Bool)) (!
    (= x ($SortWrappers.$SnapToBool($SortWrappers.BoolTo$Snap x)))
    :pattern (($SortWrappers.BoolTo$Snap x))
    )))
(declare-fun $SortWrappers.IntTo$Snap (Int) $Snap)
(declare-fun $SortWrappers.$SnapToInt ($Snap) Int)
(assert (forall ((x Int)) (!
    (= x ($SortWrappers.$SnapToInt($SortWrappers.IntTo$Snap x)))
    :pattern (($SortWrappers.IntTo$Snap x))
    )))
; Declaring additional sort wrappers
(declare-fun $SortWrappers.$Seq<Int>To$Snap ($Seq<Int>) $Snap)
(declare-fun $SortWrappers.$SnapTo$Seq<Int> ($Snap) $Seq<Int>)
(assert (forall ((x $Seq<Int>)) (!
    (= x ($SortWrappers.$SnapTo$Seq<Int>($SortWrappers.$Seq<Int>To$Snap x)))
    :pattern (($SortWrappers.$Seq<Int>To$Snap x))
    )))
(declare-fun $SortWrappers.$Seq<$Ref>To$Snap ($Seq<$Ref>) $Snap)
(declare-fun $SortWrappers.$SnapTo$Seq<$Ref> ($Snap) $Seq<$Ref>)
(assert (forall ((x $Seq<$Ref>)) (!
    (= x ($SortWrappers.$SnapTo$Seq<$Ref>($SortWrappers.$Seq<$Ref>To$Snap x)))
    :pattern (($SortWrappers.$Seq<$Ref>To$Snap x))
    )))
; Declaring additional sort wrappers
(declare-fun $SortWrappers.$Set<$Ref>To$Snap ($Set<$Ref>) $Snap)
(declare-fun $SortWrappers.$SnapTo$Set<$Ref> ($Snap) $Set<$Ref>)
(assert (forall ((x $Set<$Ref>)) (!
    (= x ($SortWrappers.$SnapTo$Set<$Ref>($SortWrappers.$Set<$Ref>To$Snap x)))
    :pattern (($SortWrappers.$Set<$Ref>To$Snap x))
    )))
(declare-fun $SortWrappers.$Set<Int>To$Snap ($Set<Int>) $Snap)
(declare-fun $SortWrappers.$SnapTo$Set<Int> ($Snap) $Set<Int>)
(assert (forall ((x $Set<Int>)) (!
    (= x ($SortWrappers.$SnapTo$Set<Int>($SortWrappers.$Set<Int>To$Snap x)))
    :pattern (($SortWrappers.$Set<Int>To$Snap x))
    )))
(declare-fun $SortWrappers.$Set<$Seq<$Ref>>To$Snap ($Set<$Seq<$Ref>>) $Snap)
(declare-fun $SortWrappers.$SnapTo$Set<$Seq<$Ref>> ($Snap) $Set<$Seq<$Ref>>)
(assert (forall ((x $Set<$Seq<$Ref>>)) (!
    (= x ($SortWrappers.$SnapTo$Set<$Seq<$Ref>>($SortWrappers.$Set<$Seq<$Ref>>To$Snap x)))
    :pattern (($SortWrappers.$Set<$Seq<$Ref>>To$Snap x))
    )))
; Declaring additional sort wrappers
(declare-fun $SortWrappers.$FVF<Int>To$Snap ($FVF<Int>) $Snap)
(declare-fun $SortWrappers.$SnapTo$FVF<Int> ($Snap) $FVF<Int>)
(assert (forall ((x $FVF<Int>)) (!
    (= x ($SortWrappers.$SnapTo$FVF<Int>($SortWrappers.$FVF<Int>To$Snap x)))
    :pattern (($SortWrappers.$FVF<Int>To$Snap x))
    )))
(declare-fun $SortWrappers.$FVF<$Seq<$Ref>>To$Snap ($FVF<$Seq<$Ref>>) $Snap)
(declare-fun $SortWrappers.$SnapTo$FVF<$Seq<$Ref>> ($Snap) $FVF<$Seq<$Ref>>)
(assert (forall ((x $FVF<$Seq<$Ref>>)) (!
    (= x ($SortWrappers.$SnapTo$FVF<$Seq<$Ref>>($SortWrappers.$FVF<$Seq<$Ref>>To$Snap x)))
    :pattern (($SortWrappers.$FVF<$Seq<$Ref>>To$Snap x))
    )))
(declare-fun $SortWrappers.$FVF<$Ref>To$Snap ($FVF<$Ref>) $Snap)
(declare-fun $SortWrappers.$SnapTo$FVF<$Ref> ($Snap) $FVF<$Ref>)
(assert (forall ((x $FVF<$Ref>)) (!
    (= x ($SortWrappers.$SnapTo$FVF<$Ref>($SortWrappers.$FVF<$Ref>To$Snap x)))
    :pattern (($SortWrappers.$FVF<$Ref>To$Snap x))
    )))
; Preamble end
; ------------------------------------------------------------
; ------------------------------------------------------------
; Declaring program functions
; ---------- main_main ----------
(declare-const this@1 $Ref)
(declare-const tcount@2 Int)
(declare-const gsize@3 Int)
(declare-const tid@4 Int)
(declare-const gid@5 Int)
(declare-const lid@6 Int)
(declare-const __last_barrier@7 Int)
(declare-const k@8 Int)
(declare-const half@9 Int)
(declare-const offset@10 Int)
(push) ; 2
; [eval] 0 <= tid
(assert (<= 0 tid@4))
; [eval] tid < tcount
(assert (< tid@4 tcount@2))
; [eval] tid == lid
(assert (= tid@4 lid@6))
; [eval] tcount == gsize
(assert (= tcount@2 gsize@3))
; [eval] gid == 0
(assert (= gid@5 0))
(assert (not (= this@1 $Ref.null)))
(declare-const $k@11 $Perm)
(assert ($Perm.isValidVar $k@11))
(assert ($Perm.isReadVar $k@11 $Perm.Write))
(declare-const $t@12 $Seq<$Ref>)
; [eval] |this.src| == gsize
; [eval] |this.src|
; (push) ; 3
; (assert (not (not (= $k@11 $Perm.No))))
; (check-sat)
; ; unsat
; ; 0.00s
; (pop) ; 3
(assert (not (= $k@11 $Perm.No)))
(assert (= ($Seq.length $t@12) gsize@3))
(declare-const $k@13 $Perm)
(assert ($Perm.isValidVar $k@13))
(assert ($Perm.isReadVar $k@13 $Perm.Write))
(declare-const $t@14 $Seq<$Ref>)
; [eval] |this.dst| == gsize
; [eval] |this.dst|
(push) ; 3 ; [XXX]
(assert (not (not (= $k@13 $Perm.No))))
(check-sat)
; unsat
; 0.00s
(pop) ; 3
; (echo "unsat")
(assert (not (= $k@13 $Perm.No)))
(assert (= ($Seq.length $t@14) gsize@3))
; [eval] 4 <= gsize
(assert (<= 4 gsize@3))
; [eval] gsize % 2 == 0
; [eval] gsize % 2
(push) ; 3
(assert (not (not (= 2 0))))
(check-sat)
; unsat
; 0.00s
(pop) ; 3
(assert (= (mod gsize@3 2) 0))
(declare-const i@15 Int)
(push) ; 3
; [eval] (i in [0..gsize))
; [eval] [0..gsize)
(assert ($Seq.contains ($Seq.range 0 gsize@3) i@15))
; [eval] this.src[i]
(push) ; 4
(assert (not (not (= gsize@3 0))))
(check-sat)
; unsat
; 0.00s
(pop) ; 4
(pop) ; 3
(declare-const $t@16 $FVF<Int>)
(declare-fun inv@17 ($Ref) Int)
(assert (forall ((r $Ref)) (!
  (implies
    ($Seq.contains ($Seq.range 0 gsize@3) i@15)
    (= ($Seq.index $t@12 (inv@17 r)) r))
  :pattern (($Seq.index $t@12 (inv@17 r))))))
(assert (forall ((i@15 Int)) (!
  (implies
    ($Seq.contains ($Seq.range 0 gsize@3) i@15)
    (= (inv@17 ($Seq.index $t@12 i@15)) i@15))
  :pattern ((inv@17 ($Seq.index $t@12 i@15)))
  ; :pattern (($Seq.contains ($Seq.range 0 gsize@3) i@15))
)))
(assert (forall ((x Int) (y Int)) (!
  (implies
    (and
      ($Seq.contains ($Seq.range 0 gsize@3) x)
      ($Seq.contains ($Seq.range 0 gsize@3) y)
      (= ($Seq.index $t@12 x) ($Seq.index $t@12 y)))
    (= x y))
  :pattern (($Seq.index $t@12 x) ($Seq.index $t@12 y)))))
(assert (forall ((i@15 Int)) (!
  (implies
    (and
      ($Seq.contains ($Seq.range 0 gsize@3) i@15)
      (< $Perm.No (/ (to_real 1) (to_real gsize@3))))
    (not (= ($Seq.index $t@12 i@15) $Ref.null)))
  :pattern (($Seq.index $t@12 i@15)))))
(assert (forall ((i@15 Int)) (!
  (iff
    ($Set.in ($Seq.index $t@12 i@15) ($FVF.domain_Integer_value $t@16))
    ($Seq.contains ($Seq.range 0 gsize@3) i@15))
  :pattern (($FVF.lookup_Integer_value $t@16 ($Seq.index $t@12 i@15))))))
(assert (< $Perm.No (/ (to_real 1) (to_real gsize@3))))
; [eval] this.dst[tid]
(assert (not (= ($Seq.index $t@14 tid@4) $Ref.null)))
(declare-const $t@18 Int)
(declare-const vs@19 $FVF<Int>)
(assert (and
  (= ($FVF.lookup_Integer_value vs@19 ($Seq.index $t@14 tid@4)) $t@18)
  ($Set.equal
    ($FVF.domain_Integer_value vs@19)
    ($Set.singleton  ($Seq.index $t@14 tid@4)))))
(push) ; 3
; [eval] 0 <= tid
; [eval] tid < tcount
; [eval] tid == lid
; [eval] tcount == gsize
; [eval] gid == 0
(declare-const $k@20 $Perm)
(assert ($Perm.isValidVar $k@20))
(assert ($Perm.isReadVar $k@20 $Perm.Write))
(declare-const $t@21 $Seq<$Ref>)
; [eval] |this.src| == gsize
; [eval] |this.src|
; (push) ; 4
; (assert (not (not (= $k@20 $Perm.No))))
; (check-sat)
; ; unsat
; ; 0.00s
; (pop) ; 4
(assert (not (= $k@20 $Perm.No)))
(assert (= ($Seq.length $t@21) gsize@3))
(declare-const $k@22 $Perm)
(assert ($Perm.isValidVar $k@22))
(assert ($Perm.isReadVar $k@22 $Perm.Write))
(declare-const $t@23 $Seq<$Ref>)
; [eval] |this.dst| == gsize
; [eval] |this.dst|
; (push) ; 4
; (assert (not (not (= $k@22 $Perm.No))))
; (check-sat)
; ; unsat
; ; 0.00s
; (pop) ; 4
(assert (not (= $k@22 $Perm.No)))
(assert (= ($Seq.length $t@23) gsize@3))
; [eval] 4 <= gsize
; [eval] gsize % 2 == 0
; [eval] gsize % 2
; (push) ; 4
; (assert (not (not (= 2 0))))
; (check-sat)
; ; unsat
; ; 0.00s
; (pop) ; 4
(declare-const i@24 Int)
(push) ; 4
; [eval] (i in [0..gsize))
; [eval] [0..gsize)
(assert ($Seq.contains ($Seq.range 0 gsize@3) i@24))
; [eval] this.src[i]
(push) ; 5
(assert (not (not (= gsize@3 0))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(pop) ; 4
(declare-const $t@25 $FVF<Int>)
(declare-fun inv@26 ($Ref) Int)
(assert (forall ((r $Ref)) (!
  (implies
    ($Seq.contains ($Seq.range 0 gsize@3) i@24)
    (= ($Seq.index $t@21 (inv@26 r)) r))
  :pattern (($Seq.index $t@21 (inv@26 r))))))
(assert (forall ((i@24 Int)) (!
  (implies
    ($Seq.contains ($Seq.range 0 gsize@3) i@24)
    (= (inv@26 ($Seq.index $t@21 i@24)) i@24))
;  :pattern (($Seq.contains ($Seq.range 0 gsize@3) i@24))
  :pattern ((inv@26 ($Seq.index $t@21 i@24))))))
(assert (forall ((x Int) (y Int)) (!
  (implies
    (and
      ($Seq.contains ($Seq.range 0 gsize@3) x)
      ($Seq.contains ($Seq.range 0 gsize@3) y)
      (= ($Seq.index $t@21 x) ($Seq.index $t@21 y)))
    (= x y))
  :pattern (($Seq.index $t@21 x) ($Seq.index $t@21 y)))))
(assert (forall ((i@24 Int)) (!
  (implies
    (and
      ($Seq.contains ($Seq.range 0 gsize@3) i@24)
      (< $Perm.No (/ (to_real 1) (to_real gsize@3))))
    (not (= ($Seq.index $t@21 i@24) $Ref.null)))
  :pattern (($Seq.index $t@21 i@24)))))
(assert (forall ((i@24 Int)) (!
  (iff
    ($Set.in ($Seq.index $t@21 i@24) ($FVF.domain_Integer_value $t@25))
    ($Seq.contains ($Seq.range 0 gsize@3) i@24))
  :pattern (($FVF.lookup_Integer_value $t@25 ($Seq.index $t@21 i@24))))))
; [eval] this.src == old(this.src)
; [eval] old(this.src)
(assert ($Seq.equal $t@21 $t@12))
; [eval] this.dst == old(this.dst)
; [eval] old(this.dst)
(assert ($Seq.equal $t@23 $t@14))
; [eval] tid == 0
(push) ; 4
(assert (not (not (= tid@4 0))))
(check-sat)
; unknown
; 0.00s
(pop) ; 4
(push) ; 4
(assert (not (= tid@4 0)))
(check-sat)
; unknown
; 0.00s
(pop) ; 4
(push) ; 4
; [then-branch 1] tid@4 == 0
(assert (= tid@4 0))
; [eval] this.dst[0]
(assert (not (= ($Seq.index $t@23 0) $Ref.null)))
(declare-const $t@27 Int)
(declare-const vs@28 $FVF<Int>)
(assert (and
  (= ($FVF.lookup_Integer_value vs@28 ($Seq.index $t@23 0)) $t@27)
  ($Set.equal
    ($FVF.domain_Integer_value vs@28)
    ($Set.singleton  ($Seq.index $t@23 0)))))
; [eval] (tid == 0 ? (forall i: Int :: (0 <= i) && (i < tcount) ==> (this.dst[0].Integer_value >= this.src[i].Integer_value)) : true)
; [eval] tid == 0
(push) ; 5
(assert (not (not (= tid@4 0))))
(check-sat)
; unknown
; 0.00s
(pop) ; 5
(push) ; 5
; [then-branch 2] tid@4 == 0
; [eval] (forall i: Int :: (0 <= i) && (i < tcount) ==> (this.dst[0].Integer_value >= this.src[i].Integer_value))
(declare-const i@29 Int)
(push) ; 6
; [eval] (0 <= i) && (i < tcount) ==> (this.dst[0].Integer_value >= this.src[i].Integer_value)
; [eval] (0 <= i) && (i < tcount)
; [eval] 0 <= i
(push) ; 7
(push) ; 8
(assert (not (not (<= 0 i@29))))
(check-sat)
; unknown
; 0.00s
(pop) ; 8
(push) ; 8
(assert (not (<= 0 i@29)))
(check-sat)
; unknown
; 0.00s
(pop) ; 8
(push) ; 8
; [then-branch 3] 0 <= i@29
(assert (<= 0 i@29))
; [eval] i < tcount
(pop) ; 8
(push) ; 8
; [else-branch 3] !0 <= i@29
(assert (not (<= 0 i@29)))
(pop) ; 8
(pop) ; 7
(push) ; 7
(push) ; 8
(assert (not (not (and (<= 0 i@29) (< i@29 tcount@2)))))
(check-sat)
; unknown
; 0.00s
(pop) ; 8
(push) ; 8
(assert (not (and (<= 0 i@29) (< i@29 tcount@2))))
(check-sat)
; unknown
; 0.00s
(pop) ; 8
(push) ; 8
; [then-branch 4] 0 <= i@29 && i@29 < tcount@2
(assert (and (<= 0 i@29) (< i@29 tcount@2)))
; [eval] this.dst[0].Integer_value >= this.src[i].Integer_value
; [eval] this.dst[0]
(push) ; 9
(assert (not (<
  $Perm.No
  (+
    (ite
      ($Seq.contains ($Seq.range 0 gsize@3) (inv@26 ($Seq.index $t@23 0)))
      (/ (to_real 1) (to_real gsize@3))
      $Perm.No)
    $Perm.Write))))
(check-sat)
; unsat
; 0.00s
(pop) ; 9
(declare-const fvf@30 $FVF<Int>)
(assert (implies
  (ite
    ($Seq.contains ($Seq.range 0 gsize@3) (inv@26 ($Seq.index $t@23 0)))
    (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
    false)
  (=
    ($FVF.lookup_Integer_value fvf@30 ($Seq.index $t@23 0))
    ($FVF.lookup_Integer_value $t@25 ($Seq.index $t@23 0)))))
(assert (=
  ($FVF.lookup_Integer_value fvf@30 ($Seq.index $t@23 0))
  ($FVF.lookup_Integer_value vs@28 ($Seq.index $t@23 0))))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@30)
  ($Set.union
    ($FVF.domain_Integer_value vs@28)
    ($FVF.domain_Integer_value $t@25))))
; [eval] this.src[i]
(push) ; 9
(assert (not (not (= ($Seq.index $t@21 i@29) $Ref.null))))
(check-sat)
; unsat
; 0.00s
(pop) ; 9
(push) ; 9
(assert (not (<
  $Perm.No
  (+
    (ite
      ($Seq.contains ($Seq.range 0 gsize@3) (inv@26 ($Seq.index $t@21 i@29)))
      (/ (to_real 1) (to_real gsize@3))
      $Perm.No)
    (ite (= ($Seq.index $t@21 i@29) ($Seq.index $t@23 0)) $Perm.Write $Perm.No)))))
(check-sat)
; unsat
; 0.00s
(pop) ; 9
(declare-const fvf@31 $FVF<Int>)
(assert (forall ((i@29 Int)) (!
  (implies
    (ite
      ($Seq.contains ($Seq.range 0 gsize@3) (inv@26 ($Seq.index $t@21 i@29)))
      (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
      false)
    (=
      ($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29))
      ($FVF.lookup_Integer_value $t@25 ($Seq.index $t@21 i@29))))
  :pattern (($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29)))
  :pattern (($FVF.lookup_Integer_value $t@25 ($Seq.index $t@21 i@29))))))
(assert (forall ((i@29 Int)) (!
  (implies
    (= ($Seq.index $t@21 i@29) ($Seq.index $t@23 0))
    (=
      ($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29))
      ($FVF.lookup_Integer_value vs@28 ($Seq.index $t@21 i@29))))
  :pattern (($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29)))
  :pattern (($FVF.lookup_Integer_value vs@28 ($Seq.index $t@21 i@29))))))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@31)
  ($Set.union
    ($FVF.domain_Integer_value vs@28)
    ($FVF.domain_Integer_value $t@25))))
(pop) ; 8
(push) ; 8
; [else-branch 4] !0 <= i@29 && i@29 < tcount@2
(assert (not (and (<= 0 i@29) (< i@29 tcount@2))))
(pop) ; 8
(pop) ; 7
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@31)
  ($Set.union
    ($FVF.domain_Integer_value vs@28)
    ($FVF.domain_Integer_value $t@25))))
(assert (forall ((i@29 Int)) (!
  (implies
    (= ($Seq.index $t@21 i@29) ($Seq.index $t@23 0))
    (=
      ($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29))
      ($FVF.lookup_Integer_value vs@28 ($Seq.index $t@21 i@29))))
  :pattern (($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29)))
  :pattern (($FVF.lookup_Integer_value vs@28 ($Seq.index $t@21 i@29))))))
(assert (forall ((i@29 Int)) (!
  (implies
    (ite
      ($Seq.contains ($Seq.range 0 gsize@3) (inv@26 ($Seq.index $t@21 i@29)))
      (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
      false)
    (=
      ($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29))
      ($FVF.lookup_Integer_value $t@25 ($Seq.index $t@21 i@29))))
  :pattern (($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29)))
  :pattern (($FVF.lookup_Integer_value $t@25 ($Seq.index $t@21 i@29))))))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@30)
  ($Set.union
    ($FVF.domain_Integer_value vs@28)
    ($FVF.domain_Integer_value $t@25))))
(assert (=
  ($FVF.lookup_Integer_value fvf@30 ($Seq.index $t@23 0))
  ($FVF.lookup_Integer_value vs@28 ($Seq.index $t@23 0))))
(assert (implies
  (ite
    ($Seq.contains ($Seq.range 0 gsize@3) (inv@26 ($Seq.index $t@23 0)))
    (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
    false)
  (=
    ($FVF.lookup_Integer_value fvf@30 ($Seq.index $t@23 0))
    ($FVF.lookup_Integer_value $t@25 ($Seq.index $t@23 0)))))
(pop) ; 6
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@31)
  ($Set.union
    ($FVF.domain_Integer_value vs@28)
    ($FVF.domain_Integer_value $t@25))))
(assert (forall ((i@29 Int)) (!
  (implies
    (= ($Seq.index $t@21 i@29) ($Seq.index $t@23 0))
    (=
      ($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29))
      ($FVF.lookup_Integer_value vs@28 ($Seq.index $t@21 i@29))))
  :pattern (($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29)))
  :pattern (($FVF.lookup_Integer_value vs@28 ($Seq.index $t@21 i@29))))))
(assert (forall ((i@29 Int)) (!
  (implies
    (ite
      ($Seq.contains ($Seq.range 0 gsize@3) (inv@26 ($Seq.index $t@21 i@29)))
      (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
      false)
    (=
      ($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29))
      ($FVF.lookup_Integer_value $t@25 ($Seq.index $t@21 i@29))))
  :pattern (($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29)))
  :pattern (($FVF.lookup_Integer_value $t@25 ($Seq.index $t@21 i@29))))))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@30)
  ($Set.union
    ($FVF.domain_Integer_value vs@28)
    ($FVF.domain_Integer_value $t@25))))
(assert (=
  ($FVF.lookup_Integer_value fvf@30 ($Seq.index $t@23 0))
  ($FVF.lookup_Integer_value vs@28 ($Seq.index $t@23 0))))
(assert (implies
  (ite
    ($Seq.contains ($Seq.range 0 gsize@3) (inv@26 ($Seq.index $t@23 0)))
    (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
    false)
  (=
    ($FVF.lookup_Integer_value fvf@30 ($Seq.index $t@23 0))
    ($FVF.lookup_Integer_value $t@25 ($Seq.index $t@23 0)))))
(pop) ; 5
; [dead else-branch 2] tid@4 != 0
(assert (ite
  (= tid@4 0)
  (and
    (implies
      (ite
        ($Seq.contains ($Seq.range 0 gsize@3) (inv@26 ($Seq.index $t@23 0)))
        (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
        false)
      (=
        ($FVF.lookup_Integer_value fvf@30 ($Seq.index $t@23 0))
        ($FVF.lookup_Integer_value $t@25 ($Seq.index $t@23 0))))
    (=
      ($FVF.lookup_Integer_value fvf@30 ($Seq.index $t@23 0))
      ($FVF.lookup_Integer_value vs@28 ($Seq.index $t@23 0)))
    ($Set.equal
      ($FVF.domain_Integer_value fvf@30)
      ($Set.union
        ($FVF.domain_Integer_value vs@28)
        ($FVF.domain_Integer_value $t@25)))
    (forall ((i@29 Int)) (!
      (implies
        (ite
          ($Seq.contains ($Seq.range 0 gsize@3) (inv@26 ($Seq.index $t@21 i@29)))
          (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
          false)
        (=
          ($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29))
          ($FVF.lookup_Integer_value $t@25 ($Seq.index $t@21 i@29))))
      :pattern (($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29)))
      :pattern (($FVF.lookup_Integer_value $t@25 ($Seq.index $t@21 i@29)))))
    (forall ((i@29 Int)) (!
      (implies
        (= ($Seq.index $t@21 i@29) ($Seq.index $t@23 0))
        (=
          ($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29))
          ($FVF.lookup_Integer_value vs@28 ($Seq.index $t@21 i@29))))
      :pattern (($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29)))
      :pattern (($FVF.lookup_Integer_value vs@28 ($Seq.index $t@21 i@29)))))
    ($Set.equal
      ($FVF.domain_Integer_value fvf@31)
      ($Set.union
        ($FVF.domain_Integer_value vs@28)
        ($FVF.domain_Integer_value $t@25))))
  true))
(declare-const $deadElse@32 Bool)
(assert (ite
  (= tid@4 0)
  (forall ((i@29 Int)) (!
    (implies
      (and (<= 0 i@29) (< i@29 tcount@2))
      (>=
        ($FVF.lookup_Integer_value fvf@30 ($Seq.index $t@23 0))
        ($FVF.lookup_Integer_value fvf@31 ($Seq.index $t@21 i@29))))
    :pattern (($Seq.index $t@21 i@29))))
  $deadElse@32))
(pop) ; 4
(push) ; 4
; [else-branch 1] tid@4 != 0
(assert (not (= tid@4 0)))
; [eval] (tid == 0 ? (forall i: Int :: (0 <= i) && (i < tcount) ==> (this.dst[0].Integer_value >= this.src[i].Integer_value)) : true)
; [eval] tid == 0
(push) ; 5
(assert (not (= tid@4 0)))
(check-sat)
; unknown
; 0.00s
(pop) ; 5
; [dead then-branch 5] tid@4 == 0
(push) ; 5
; [else-branch 5] tid@4 != 0
(pop) ; 5
(declare-const $deadThen@33 Bool)
(assert (ite (= tid@4 0) $deadThen@33 true))
(pop) ; 4
(pop) ; 3
(push) ; 3
; [exec]
; __last_barrier := 0
; [exec]
; half := gsize \ 2
; [eval] gsize \ 2
(push) ; 4
(assert (not (not (= 2 0))))
(check-sat)
; unsat
; 0.00s
(pop) ; 4
; [exec]
; offset := (tid == 0 ? 0 : half)
; [eval] (tid == 0 ? 0 : half)
; [eval] tid == 0
(push) ; 4
(assert (not (not (= tid@4 0))))
(check-sat)
; unknown
; 0.00s
(pop) ; 4
(push) ; 4
(assert (not (= tid@4 0)))
(check-sat)
; unknown
; 0.00s
(pop) ; 4
(push) ; 4
; [then-branch 6] tid@4 == 0
(assert (= tid@4 0))
(pop) ; 4
(push) ; 4
; [else-branch 6] tid@4 != 0
(assert (not (= tid@4 0)))
(pop) ; 4
(assert (ite (= tid@4 0) true (not (= tid@4 0))))
; [eval] tid < 2
(push) ; 4
(assert (not (not (< tid@4 2))))
(check-sat)
; unknown
; 0.00s
(pop) ; 4
(push) ; 4
(assert (not (< tid@4 2)))
(check-sat)
; unknown
; 0.00s
(pop) ; 4
(push) ; 4
; [then-branch 7] tid@4 < 2
(assert (< tid@4 2))
; [exec]
; this.dst[tid].Integer_value := this.src[offset].Integer_value
; [eval] this.dst[tid]
; [eval] this.src[offset]
(push) ; 5
(assert (not (not (= ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2))) $Ref.null))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(push) ; 5
(assert (not (<
  $Perm.No
  (+
    (ite
      ($Seq.contains
        ($Seq.range 0 gsize@3)
        (inv@17 ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2)))))
      (/ (to_real 1) (to_real gsize@3))
      $Perm.No)
    (ite
      (=
        ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2)))
        ($Seq.index $t@14 tid@4))
      $Perm.Write
      $Perm.No)))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(declare-const fvf@34 $FVF<Int>)
(assert (implies
  (ite
    ($Seq.contains
      ($Seq.range 0 gsize@3)
      (inv@17 ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2)))))
    (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
    false)
  (=
    ($FVF.lookup_Integer_value fvf@34 ($Seq.index
      $t@12
      (ite (= tid@4 0) 0 (div gsize@3 2))))
    ($FVF.lookup_Integer_value $t@16 ($Seq.index
      $t@12
      (ite (= tid@4 0) 0 (div gsize@3 2)))))))
(assert (implies
  (=
    ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2)))
    ($Seq.index $t@14 tid@4))
  (=
    ($FVF.lookup_Integer_value fvf@34 ($Seq.index
      $t@12
      (ite (= tid@4 0) 0 (div gsize@3 2))))
    ($FVF.lookup_Integer_value vs@19 ($Seq.index
      $t@12
      (ite (= tid@4 0) 0 (div gsize@3 2)))))))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@34)
  ($Set.union
    ($FVF.domain_Integer_value vs@19)
    ($FVF.domain_Integer_value $t@16))))
(declare-const sk@35 $Ref)
(declare-const vs@36 $FVF<Int>)
(push) ; 5
(assert (not (forall ((r $Ref)) (!
  (=
    (-
      (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
      ($Perm.min
        (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
        (ite
          (= r ($Seq.index $t@14 tid@4))
          (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
          $Perm.No)))
    $Perm.No)
  ))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(push) ; 5
(assert (not (=
  (-
    (ite (= sk@35 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
    ($Perm.min
      (ite (= sk@35 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
      (ite
        (= sk@35 ($Seq.index $t@14 tid@4))
        (ite (= sk@35 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
        $Perm.No)))
  $Perm.No)))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(assert (forall ((sk@35 $Ref)) (!
  (implies
    (= sk@35 ($Seq.index $t@14 tid@4))
    (=
      ($FVF.lookup_Integer_value vs@36 sk@35)
      ($FVF.lookup_Integer_value vs@19 sk@35)))
  :pattern (($FVF.lookup_Integer_value vs@36 sk@35))
  :pattern (($FVF.lookup_Integer_value vs@19 sk@35)))))
(assert (forall ((sk@35 $Ref)) (!
  (implies
    (ite
      ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 sk@35))
      (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
      false)
    (=
      ($FVF.lookup_Integer_value vs@36 sk@35)
      ($FVF.lookup_Integer_value $t@16 sk@35)))
  :pattern (($FVF.lookup_Integer_value vs@36 sk@35))
  :pattern (($FVF.lookup_Integer_value $t@16 sk@35)))))
(assert ($Set.equal
  ($FVF.domain_Integer_value vs@36)
  ($Set.union
    ($FVF.domain_Integer_value $t@16)
    ($FVF.domain_Integer_value vs@19))))
(declare-const vs@37 $FVF<Int>)
(assert (and
  (=
    ($FVF.lookup_Integer_value vs@37 ($Seq.index $t@14 tid@4))
    ($FVF.lookup_Integer_value fvf@34 ($Seq.index
      $t@12
      (ite (= tid@4 0) 0 (div gsize@3 2)))))
  ($Set.equal
    ($FVF.domain_Integer_value vs@37)
    ($Set.singleton  ($Seq.index $t@14 tid@4)))))
; [exec]
; k := 0
; [exec]
; assert this.dst[tid].Integer_value >= this.src[offset].Integer_value
; [eval] this.dst[tid].Integer_value >= this.src[offset].Integer_value
; [eval] this.dst[tid]
(push) ; 5
(assert (not (<
  $Perm.No
  (+
    (ite
      ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 ($Seq.index $t@14 tid@4)))
      (/ (to_real 1) (to_real gsize@3))
      $Perm.No)
    $Perm.Write))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(declare-const fvf@38 $FVF<Int>)
(assert (implies
  (ite
    ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 ($Seq.index $t@14 tid@4)))
    (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
    false)
  (=
    ($FVF.lookup_Integer_value fvf@38 ($Seq.index $t@14 tid@4))
    ($FVF.lookup_Integer_value $t@16 ($Seq.index $t@14 tid@4)))))
(assert (=
  ($FVF.lookup_Integer_value fvf@38 ($Seq.index $t@14 tid@4))
  ($FVF.lookup_Integer_value vs@37 ($Seq.index $t@14 tid@4))))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@38)
  ($Set.union
    ($FVF.domain_Integer_value vs@37)
    ($FVF.domain_Integer_value $t@16))))
; [eval] this.src[offset]
(push) ; 5
(assert (not (not (= ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2))) $Ref.null))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(push) ; 5
(assert (not (<
  $Perm.No
  (+
    (ite
      ($Seq.contains
        ($Seq.range 0 gsize@3)
        (inv@17 ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2)))))
      (/ (to_real 1) (to_real gsize@3))
      $Perm.No)
    (ite
      (=
        ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2)))
        ($Seq.index $t@14 tid@4))
      $Perm.Write
      $Perm.No)))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(declare-const fvf@39 $FVF<Int>)
(assert (implies
  (ite
    ($Seq.contains
      ($Seq.range 0 gsize@3)
      (inv@17 ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2)))))
    (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
    false)
  (=
    ($FVF.lookup_Integer_value fvf@39 ($Seq.index
      $t@12
      (ite (= tid@4 0) 0 (div gsize@3 2))))
    ($FVF.lookup_Integer_value $t@16 ($Seq.index
      $t@12
      (ite (= tid@4 0) 0 (div gsize@3 2)))))))
(assert (implies
  (=
    ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2)))
    ($Seq.index $t@14 tid@4))
  (=
    ($FVF.lookup_Integer_value fvf@39 ($Seq.index
      $t@12
      (ite (= tid@4 0) 0 (div gsize@3 2))))
    ($FVF.lookup_Integer_value vs@37 ($Seq.index
      $t@12
      (ite (= tid@4 0) 0 (div gsize@3 2)))))))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@39)
  ($Set.union
    ($FVF.domain_Integer_value vs@37)
    ($FVF.domain_Integer_value $t@16))))
(push) ; 5
(assert (not (>=
  ($FVF.lookup_Integer_value fvf@38 ($Seq.index $t@14 tid@4))
  ($FVF.lookup_Integer_value fvf@39 ($Seq.index
    $t@12
    (ite (= tid@4 0) 0 (div gsize@3 2)))))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(assert (>=
  ($FVF.lookup_Integer_value fvf@38 ($Seq.index $t@14 tid@4))
  ($FVF.lookup_Integer_value fvf@39 ($Seq.index
    $t@12
    (ite (= tid@4 0) 0 (div gsize@3 2))))))
; [exec]
; assert this.dst[tid].Integer_value >= this.src[offset + 0].Integer_value
; [eval] this.dst[tid].Integer_value >= this.src[offset + 0].Integer_value
; [eval] this.dst[tid]
(push) ; 5
(assert (not (<
  $Perm.No
  (+
    (ite
      ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 ($Seq.index $t@14 tid@4)))
      (/ (to_real 1) (to_real gsize@3))
      $Perm.No)
    $Perm.Write))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(declare-const fvf@40 $FVF<Int>)
; [eval] this.src[offset + 0]
; [eval] offset + 0
(push) ; 5
(assert (not (not (= ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2))) $Ref.null))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(push) ; 5
(assert (not (<
  $Perm.No
  (+
    (ite
      ($Seq.contains
        ($Seq.range 0 gsize@3)
        (inv@17 ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2)))))
      (/ (to_real 1) (to_real gsize@3))
      $Perm.No)
    (ite
      (=
        ($Seq.index $t@12 (ite (= tid@4 0) 0 (div gsize@3 2)))
        ($Seq.index $t@14 tid@4))
      $Perm.Write
      $Perm.No)))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(declare-const fvf@41 $FVF<Int>)
; [exec]
; assert (forall i: Int :: (0 <= i) && (i < k) ==> (this.dst[tid].Integer_value >= this.src[offset + i].Integer_value))
; [eval] (forall i: Int :: (0 <= i) && (i < k) ==> (this.dst[tid].Integer_value >= this.src[offset + i].Integer_value))
(declare-const i@42 Int)
(push) ; 5
; [eval] (0 <= i) && (i < k) ==> (this.dst[tid].Integer_value >= this.src[offset + i].Integer_value)
; [eval] (0 <= i) && (i < k)
; [eval] 0 <= i
(push) ; 6
(push) ; 7
(assert (not (not (<= 0 i@42))))
(check-sat)
; unknown
; 0.01s
(pop) ; 7
(push) ; 7
(assert (not (<= 0 i@42)))
(check-sat)
; unknown
; 0.01s
(pop) ; 7
(push) ; 7
; [then-branch 8] 0 <= i@42
(assert (<= 0 i@42))
; [eval] i < k
(pop) ; 7
(push) ; 7
; [else-branch 8] !0 <= i@42
(assert (not (<= 0 i@42)))
(pop) ; 7
(pop) ; 6
(push) ; 6
(push) ; 7
(assert (not (not (and (<= 0 i@42) (< i@42 0)))))
(check-sat)
; unsat
; 0.00s
(pop) ; 7
(push) ; 7
(assert (not (and (<= 0 i@42) (< i@42 0))))
(check-sat)
; unknown
; 0.01s
(pop) ; 7
; [dead then-branch 9] 0 <= i@42 && i@42 < 0
(push) ; 7
; [else-branch 9] !0 <= i@42 && i@42 < 0
(assert (not (and (<= 0 i@42) (< i@42 0))))
(pop) ; 7
(pop) ; 6
(pop) ; 5
(push) ; 5
(assert (not (forall ((i@42 Int)) (!
  true
  ))))
(check-sat)
; unsat
; 0.00s
(pop) ; 5
(assert (forall ((i@42 Int)) (!
  true
  )))
; loop at max-two-range.sil,53:5
(declare-const k@43 Int)
(push) ; 5
; Verify loop body
(declare-const $t@44 $Snap)
(declare-const $t@45 $Snap)
(assert (= $t@44 ($Snap.combine $t@45 $Snap.unit)))
(declare-const $t@46 $Snap)
(assert (= $t@45 ($Snap.combine $t@46 $Snap.unit)))
(declare-const $t@47 $Snap)
(assert (= $t@46 ($Snap.combine $t@47 $Snap.unit)))
(declare-const $t@48 $Snap)
(declare-const $t@49 Int)
(assert (= $t@47 ($Snap.combine $t@48 ($SortWrappers.IntTo$Snap $t@49))))
(declare-const $t@50 $Snap)
(declare-const $t@51 $Snap)
(assert (= $t@48 ($Snap.combine $t@50 $t@51)))
(declare-const $t@52 $Snap)
(assert (= $t@50 ($Snap.combine $t@52 $Snap.unit)))
(declare-const $t@53 $Snap)
(declare-const $t@54 $FVF<Int>)
(assert (= $t@52 ($Snap.combine $t@53 ($SortWrappers.$FVF<Int>To$Snap $t@54))))
(declare-const $t@55 $Snap)
(assert (= $t@53 ($Snap.combine $t@55 $Snap.unit)))
(declare-const $t@56 $Snap)
(assert (= $t@55 ($Snap.combine $t@56 $Snap.unit)))
(declare-const $t@57 $Snap)
(assert (= $t@56 ($Snap.combine $t@57 $Snap.unit)))
(declare-const $t@58 $Snap)
(assert (= $t@57 ($Snap.combine $t@58 $Snap.unit)))
(declare-const $t@59 $Seq<$Ref>)
(declare-const $t@60 $Seq<$Ref>)
(assert (=
  $t@58
  ($Snap.combine
    ($SortWrappers.$Seq<$Ref>To$Snap $t@59)
    ($SortWrappers.$Seq<$Ref>To$Snap $t@60))))
(declare-const $t@61 $Seq<$Ref>)
(assert (=
  ($SortWrappers.$Seq<$Ref>To$Snap $t@59)
  ($Snap.combine ($SortWrappers.$Seq<$Ref>To$Snap $t@61) $Snap.unit)))
(declare-const $t@62 $Seq<$Ref>)
(assert (=
  ($SortWrappers.$Seq<$Ref>To$Snap $t@61)
  ($Snap.combine $Snap.unit ($SortWrappers.$Seq<$Ref>To$Snap $t@62))))
; [eval] (0 <= tid) && (tid < tcount) && (tid == lid) && (tcount == gsize) && (gid == 0)
; [eval] (0 <= tid) && (tid < tcount) && (tid == lid) && (tcount == gsize)
; [eval] (0 <= tid) && (tid < tcount) && (tid == lid)
; [eval] (0 <= tid) && (tid < tcount)
; [eval] 0 <= tid
(push) ; 6
(push) ; 7
(assert (not (not (<= 0 tid@4))))
(check-sat)
; unknown
; 0.01s
(pop) ; 7
(push) ; 7
; [then-branch 10] 0 <= tid@4
; [eval] tid < tcount
(pop) ; 7
; [dead else-branch 10] !0 <= tid@4
(pop) ; 6
(push) ; 6
(push) ; 7
(assert (not (not (and (<= 0 tid@4) (< tid@4 tcount@2)))))
(check-sat)
; unknown
; 0.01s
(pop) ; 7
(push) ; 7
(assert (not (and (<= 0 tid@4) (< tid@4 tcount@2))))
(check-sat)
; unsat
; 0.00s
(pop) ; 7
(push) ; 7
; [then-branch 11] 0 <= tid@4 && tid@4 < tcount@2
(assert (and (<= 0 tid@4) (< tid@4 tcount@2)))
; [eval] tid == lid
(pop) ; 7
; [dead else-branch 11] !0 <= tid@4 && tid@4 < tcount@2
(pop) ; 6
(push) ; 6
(push) ; 7
(assert (not (not (and (and (<= 0 tid@4) (< tid@4 tcount@2)) (= tid@4 lid@6)))))
(check-sat)
; unknown
; 0.01s
(pop) ; 7
(push) ; 7
(assert (not (and (and (<= 0 tid@4) (< tid@4 tcount@2)) (= tid@4 lid@6))))
(check-sat)
; unsat
; 0.00s
(pop) ; 7
(push) ; 7
; [then-branch 12] 0 <= tid@4 && tid@4 < tcount@2 && tid@4 == lid@6
(assert (and (and (<= 0 tid@4) (< tid@4 tcount@2)) (= tid@4 lid@6)))
; [eval] tcount == gsize
(pop) ; 7
; [dead else-branch 12] !0 <= tid@4 && tid@4 < tcount@2 && tid@4 == lid@6
(pop) ; 6
(push) ; 6
(push) ; 7
(assert (not (not
  (and
    (and (and (<= 0 tid@4) (< tid@4 tcount@2)) (= tid@4 lid@6))
    (= tcount@2 gsize@3)))))
(check-sat)
; unknown
; 0.01s
(pop) ; 7
(push) ; 7
(assert (not (and
  (and (and (<= 0 tid@4) (< tid@4 tcount@2)) (= tid@4 lid@6))
  (= tcount@2 gsize@3))))
(check-sat)
; unsat
; 0.00s
(pop) ; 7
(push) ; 7
; [then-branch 13] 0 <= tid@4 && tid@4 < tcount@2 && tid@4 == lid@6 && tcount@2 == gsize@3
(assert (and
  (and (and (<= 0 tid@4) (< tid@4 tcount@2)) (= tid@4 lid@6))
  (= tcount@2 gsize@3)))
; [eval] gid == 0
(pop) ; 7
; [dead else-branch 13] !0 <= tid@4 && tid@4 < tcount@2 && tid@4 == lid@6 && tcount@2 == gsize@3
(pop) ; 6
(assert (and
  (and
    (and (and (<= 0 tid@4) (< tid@4 tcount@2)) (= tid@4 lid@6))
    (= tcount@2 gsize@3))
  (= gid@5 0)))
(declare-const $k@63 $Perm)
(assert ($Perm.isValidVar $k@63))
(assert ($Perm.isReadVar $k@63 $Perm.Write))
; [eval] |this.src| == gsize
; [eval] |this.src|
(push) ; 6
(assert (not (not (= $k@63 $Perm.No))))
(check-sat)
; unsat
; 0.00s
(pop) ; 6
(assert (not (= $k@63 $Perm.No)))
(assert (= ($Seq.length $t@62) gsize@3))
(declare-const $k@64 $Perm)
(assert ($Perm.isValidVar $k@64))
(assert ($Perm.isReadVar $k@64 $Perm.Write))
; [eval] |this.dst| == gsize
; [eval] |this.dst|
(push) ; 6
(assert (not (not (= $k@64 $Perm.No))))
(check-sat)
; unsat
; 0.00s
(pop) ; 6
(assert (not (= $k@64 $Perm.No)))
(assert (= ($Seq.length $t@60) gsize@3))
; [eval] 4 <= gsize
; [eval] gsize % 2 == 0
; [eval] gsize % 2
(push) ; 6
(assert (not (not (= 2 0))))
(check-sat)
; unsat
; 0.00s
(pop) ; 6
; [eval] offset == (tid == 0 ? 0 : half)
; [eval] (tid == 0 ? 0 : half)
; [eval] tid == 0
(push) ; 6
(assert (not (not (= tid@4 0))))
(check-sat)
; unknown
; 0.01s
(pop) ; 6
(push) ; 6
(assert (not (= tid@4 0)))
(check-sat)
; unknown
; 0.01s
(pop) ; 6
(push) ; 6
; [then-branch 14] tid@4 == 0
(assert (= tid@4 0))
(pop) ; 6
(push) ; 6
; [else-branch 14] tid@4 != 0
(assert (not (= tid@4 0)))
(pop) ; 6
(declare-const i@65 Int)
(push) ; 6
; [eval] (i in [0..gsize))
; [eval] [0..gsize)
(assert ($Seq.contains ($Seq.range 0 gsize@3) i@65))
; [eval] this.src[i]
(push) ; 7
(assert (not (not (= gsize@3 0))))
(check-sat)
; unsat
; 0.00s
(pop) ; 7
(pop) ; 6
(declare-fun inv@66 ($Ref) Int)
(assert (forall ((r $Ref)) (!
  (implies
    ($Seq.contains ($Seq.range 0 gsize@3) i@65)
    (= ($Seq.index $t@62 (inv@66 r)) r))
  :pattern (($Seq.index $t@62 (inv@66 r))))))
(assert (forall ((i@65 Int)) (!
  (implies
    ($Seq.contains ($Seq.range 0 gsize@3) i@65)
    (= (inv@66 ($Seq.index $t@62 i@65)) i@65))
;  :pattern (($Seq.contains ($Seq.range 0 gsize@3) i@65))
  :pattern ((inv@66 ($Seq.index $t@62 i@65))))))
(assert (forall ((x Int) (y Int)) (!
  (implies
    (and
      ($Seq.contains ($Seq.range 0 gsize@3) x)
      ($Seq.contains ($Seq.range 0 gsize@3) y)
      (= ($Seq.index $t@62 x) ($Seq.index $t@62 y)))
    (= x y))
  :pattern (($Seq.index $t@62 x) ($Seq.index $t@62 y)))))
(assert (forall ((i@65 Int)) (!
  (implies
    (and
      ($Seq.contains ($Seq.range 0 gsize@3) i@65)
      (< $Perm.No (/ (to_real 1) (to_real gsize@3))))
    (not (= ($Seq.index $t@62 i@65) $Ref.null)))
  :pattern (($Seq.index $t@62 i@65)))))
(assert (forall ((i@65 Int)) (!
  (iff
    ($Set.in ($Seq.index $t@62 i@65) ($FVF.domain_Integer_value $t@54))
    ($Seq.contains ($Seq.range 0 gsize@3) i@65))
  :pattern (($FVF.lookup_Integer_value $t@54 ($Seq.index $t@62 i@65))))))
; [eval] false || (__last_barrier == 0)
(push) ; 6
(push) ; 7
(assert (not false))
(check-sat)
; unknown
; 0.01s
(pop) ; 7
(push) ; 7
; [then-branch 15] True
; [eval] __last_barrier == 0
(pop) ; 7
; [dead else-branch 15] False
(pop) ; 6
; [eval] __last_barrier == 1
(push) ; 6
(assert (not (not (= 0 1))))
(check-sat)
; unsat
; 0.00s
(pop) ; 6
(push) ; 6
(assert (not (= 0 1)))
(check-sat)
; unknown
; 0.01s
(pop) ; 6
; [dead then-branch 16] 0 == 1
(push) ; 6
; [else-branch 16] 0 != 1
(assert (not (= 0 1)))
; [eval] __last_barrier == 0
(push) ; 7
(assert (not false))
(check-sat)
; unknown
; 0.01s
(pop) ; 7
(push) ; 7
; [then-branch 17] True
; [eval] this.dst[tid]
(assert (not (= ($Seq.index $t@60 tid@4) $Ref.null)))
(declare-const vs@67 $FVF<Int>)
(assert (and
  (= ($FVF.lookup_Integer_value vs@67 ($Seq.index $t@60 tid@4)) $t@49)
  ($Set.equal
    ($FVF.domain_Integer_value vs@67)
    ($Set.singleton  ($Seq.index $t@60 tid@4)))))
; [eval] (0 <= k) && (k <= half)
; [eval] 0 <= k
(push) ; 8
(push) ; 9
(assert (not (not (<= 0 k@43))))
(check-sat)
; unknown
; 0.02s
(pop) ; 9
(push) ; 9
(assert (not (<= 0 k@43)))
(check-sat)
; unknown
; 0.02s
(pop) ; 9
(push) ; 9
; [then-branch 18] 0 <= k@43
(assert (<= 0 k@43))
; [eval] k <= half
(pop) ; 9
(push) ; 9
; [else-branch 18] !0 <= k@43
(assert (not (<= 0 k@43)))
(pop) ; 9
(pop) ; 8
(assert (and (<= 0 k@43) (<= k@43 (div gsize@3 2))))
; [eval] (forall i: Int :: (0 <= i) && (i < k) ==> (this.dst[tid].Integer_value >= this.src[offset + i].Integer_value))
(declare-const i@68 Int)
(push) ; 8
; [eval] (0 <= i) && (i < k) ==> (this.dst[tid].Integer_value >= this.src[offset + i].Integer_value)
; [eval] (0 <= i) && (i < k)
; [eval] 0 <= i
(push) ; 9
(push) ; 10
(assert (not (not (<= 0 i@68))))
(check-sat)
; unknown
; 0.02s
(pop) ; 10
(push) ; 10
(assert (not (<= 0 i@68)))
(check-sat)
; unknown
; 0.02s
(pop) ; 10
(push) ; 10
; [then-branch 19] 0 <= i@68
(assert (<= 0 i@68))
; [eval] i < k
(pop) ; 10
(push) ; 10
; [else-branch 19] !0 <= i@68
(assert (not (<= 0 i@68)))
(pop) ; 10
(pop) ; 9
(push) ; 9
(push) ; 10
(assert (not (not (and (<= 0 i@68) (< i@68 k@43)))))
(check-sat)
; unknown
; 0.02s
(pop) ; 10
(push) ; 10
(assert (not (and (<= 0 i@68) (< i@68 k@43))))
(check-sat)
; unknown
; 0.02s
(pop) ; 10
(push) ; 10
; [then-branch 20] 0 <= i@68 && i@68 < k@43
(assert (and (<= 0 i@68) (< i@68 k@43)))
; [eval] this.dst[tid].Integer_value >= this.src[offset + i].Integer_value
; [eval] this.dst[tid]
(push) ; 11
(assert (not (<
  $Perm.No
  (+
    (ite
      ($Seq.contains ($Seq.range 0 gsize@3) (inv@66 ($Seq.index $t@60 tid@4)))
      (/ (to_real 1) (to_real gsize@3))
      $Perm.No)
    $Perm.Write))))
(check-sat)
; unsat
; 0.00s
(pop) ; 11
(declare-const fvf@69 $FVF<Int>)
(assert (implies
  (ite
    ($Seq.contains ($Seq.range 0 gsize@3) (inv@66 ($Seq.index $t@60 tid@4)))
    (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
    false)
  (=
    ($FVF.lookup_Integer_value fvf@69 ($Seq.index $t@60 tid@4))
    ($FVF.lookup_Integer_value $t@54 ($Seq.index $t@60 tid@4)))))
(assert (=
  ($FVF.lookup_Integer_value fvf@69 ($Seq.index $t@60 tid@4))
  ($FVF.lookup_Integer_value vs@67 ($Seq.index $t@60 tid@4))))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@69)
  ($Set.union
    ($FVF.domain_Integer_value vs@67)
    ($FVF.domain_Integer_value $t@54))))
; [eval] this.src[offset + i]
; [eval] offset + i
(push) ; 11
(assert (not (not
  (= ($Seq.index $t@62 (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)) $Ref.null))))
(check-sat)
; unsat
; 0.01s
(pop) ; 11
(push) ; 11
(assert (not (<
  $Perm.No
  (+
    (ite
      ($Seq.contains
        ($Seq.range 0 gsize@3)
        (inv@66 ($Seq.index $t@62 (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68))))
      (/ (to_real 1) (to_real gsize@3))
      $Perm.No)
    (ite
      (=
        ($Seq.index $t@62 (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68))
        ($Seq.index $t@60 tid@4))
      $Perm.Write
      $Perm.No)))))
(check-sat)
; unsat
(pop) ; 11
(declare-const fvf@70 $FVF<Int>)
(assert (forall ((i@68 Int)) (!
  (implies
    (ite
      ($Seq.contains
        ($Seq.range 0 gsize@3)
        (inv@66 ($Seq.index $t@62 (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68))))
      (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
      false)
    (=
      ($FVF.lookup_Integer_value fvf@70 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))
      ($FVF.lookup_Integer_value $t@54 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))))
  )))
(assert (forall ((i@68 Int)) (!
  (implies
    (=
      ($Seq.index $t@62 (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68))
      ($Seq.index $t@60 tid@4))
    (=
      ($FVF.lookup_Integer_value fvf@70 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))
      ($FVF.lookup_Integer_value vs@67 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))))
  )))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@70)
  ($Set.union
    ($FVF.domain_Integer_value vs@67)
    ($FVF.domain_Integer_value $t@54))))
(pop) ; 10
(push) ; 10
; [else-branch 20] !0 <= i@68 && i@68 < k@43
(assert (not (and (<= 0 i@68) (< i@68 k@43))))
(pop) ; 10
(pop) ; 9
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@70)
  ($Set.union
    ($FVF.domain_Integer_value vs@67)
    ($FVF.domain_Integer_value $t@54))))
(assert (forall ((i@68 Int)) (!
  (implies
    (=
      ($Seq.index $t@62 (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68))
      ($Seq.index $t@60 tid@4))
    (=
      ($FVF.lookup_Integer_value fvf@70 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))
      ($FVF.lookup_Integer_value vs@67 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))))
  )))
(assert (forall ((i@68 Int)) (!
  (implies
    (ite
      ($Seq.contains
        ($Seq.range 0 gsize@3)
        (inv@66 ($Seq.index $t@62 (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68))))
      (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
      false)
    (=
      ($FVF.lookup_Integer_value fvf@70 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))
      ($FVF.lookup_Integer_value $t@54 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))))
  )))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@69)
  ($Set.union
    ($FVF.domain_Integer_value vs@67)
    ($FVF.domain_Integer_value $t@54))))
(assert (=
  ($FVF.lookup_Integer_value fvf@69 ($Seq.index $t@60 tid@4))
  ($FVF.lookup_Integer_value vs@67 ($Seq.index $t@60 tid@4))))
(assert (implies
  (ite
    ($Seq.contains ($Seq.range 0 gsize@3) (inv@66 ($Seq.index $t@60 tid@4)))
    (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
    false)
  (=
    ($FVF.lookup_Integer_value fvf@69 ($Seq.index $t@60 tid@4))
    ($FVF.lookup_Integer_value $t@54 ($Seq.index $t@60 tid@4)))))
(pop) ; 8
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@70)
  ($Set.union
    ($FVF.domain_Integer_value vs@67)
    ($FVF.domain_Integer_value $t@54))))
(assert (forall ((i@68 Int)) (!
  (implies
    (=
      ($Seq.index $t@62 (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68))
      ($Seq.index $t@60 tid@4))
    (=
      ($FVF.lookup_Integer_value fvf@70 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))
      ($FVF.lookup_Integer_value vs@67 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))))
  )))
(assert (forall ((i@68 Int)) (!
  (implies
    (ite
      ($Seq.contains
        ($Seq.range 0 gsize@3)
        (inv@66 ($Seq.index $t@62 (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68))))
      (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
      false)
    (=
      ($FVF.lookup_Integer_value fvf@70 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))
      ($FVF.lookup_Integer_value $t@54 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))))
  )))
(assert ($Set.equal
  ($FVF.domain_Integer_value fvf@69)
  ($Set.union
    ($FVF.domain_Integer_value vs@67)
    ($FVF.domain_Integer_value $t@54))))
(assert (=
  ($FVF.lookup_Integer_value fvf@69 ($Seq.index $t@60 tid@4))
  ($FVF.lookup_Integer_value vs@67 ($Seq.index $t@60 tid@4))))
(assert (implies
  (ite
    ($Seq.contains ($Seq.range 0 gsize@3) (inv@66 ($Seq.index $t@60 tid@4)))
    (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
    false)
  (=
    ($FVF.lookup_Integer_value fvf@69 ($Seq.index $t@60 tid@4))
    ($FVF.lookup_Integer_value $t@54 ($Seq.index $t@60 tid@4)))))
(assert (forall ((i@68 Int)) (!
  (implies
    (and (<= 0 i@68) (< i@68 k@43))
    (>=
      ($FVF.lookup_Integer_value fvf@69 ($Seq.index $t@60 tid@4))
      ($FVF.lookup_Integer_value fvf@70 ($Seq.index
        $t@62
        (+ (ite (= tid@4 0) 0 (div gsize@3 2)) i@68)))))
  )))
; [eval] k < half
(assert (< k@43 (div gsize@3 2)))
(check-sat)
; unknown
; [exec]
; inhale false
(pop) ; 7
; [dead else-branch 17] False
(pop) ; 6
(pop) ; 5
(push) ; 5
; Establish loop invariant
; [eval] 0 <= tid
; [eval] tid < tcount
; [eval] tid == lid
; [eval] tcount == gsize
; [eval] gid == 0
(declare-const $k@71 $Perm)
(assert ($Perm.isValidVar $k@71))
(assert ($Perm.isReadVar $k@71 $Perm.Write))
(assert (< $k@71 $k@11))
; [eval] |this.src| == gsize
; [eval] |this.src|
(declare-const $k@72 $Perm)
(assert ($Perm.isValidVar $k@72))
(assert ($Perm.isReadVar $k@72 $Perm.Write))
(assert (< $k@72 $k@13))
; [eval] |this.dst| == gsize
; [eval] |this.dst|
; [eval] 4 <= gsize
; [eval] gsize % 2 == 0
; [eval] gsize % 2
(push) ; 6
(assert (not (not (= 2 0))))
(check-sat)
; unsat
; 0.00s
(pop) ; 6
; [eval] offset == (tid == 0 ? 0 : half)
; [eval] (tid == 0 ? 0 : half)
; [eval] tid == 0
(push) ; 6
(assert (not (not (= tid@4 0))))
(check-sat)
; unknown
; 0.01s
(pop) ; 6
(push) ; 6
(assert (not (= tid@4 0)))
(check-sat)
; unknown
; 0.01s
(pop) ; 6
(push) ; 6
; [then-branch 21] tid@4 == 0
(assert (= tid@4 0))
(pop) ; 6
(push) ; 6
; [else-branch 21] tid@4 != 0
(assert (not (= tid@4 0)))
(pop) ; 6
(declare-const i@73 Int)
(declare-const vs@74 $FVF<$Seq<$Ref>>)
(assert (and
  ($Seq.equal ($FVF.lookup_src vs@74 this@1) $t@12)
  ($Set.equal ($FVF.domain_src vs@74) ($Set.singleton  this@1))))
; [eval] (i in [0..gsize))
; [eval] [0..gsize)
(push) ; 6
(assert (not (not ($Seq.contains ($Seq.range 0 gsize@3) i@73))))
(check-sat)
; unknown
(pop) ; 6
(assert ($Seq.contains ($Seq.range 0 gsize@3) i@73))
(push) ; 6
(assert (not (not (= gsize@3 0))))
(check-sat)
; unsat
; 0.00s
(pop) ; 6
(push) ; 6
(assert (not (or
  (= (/ (to_real 1) (to_real gsize@3)) $Perm.No)
  (< $Perm.No (/ (to_real 1) (to_real gsize@3))))))
(check-sat)
; unsat
; 0.00s
(pop) ; 6
; [eval] this.src[i]
(push) ; 6
(assert (not (< $Perm.No $k@11)))
(check-sat)
; unsat
; 0.00s
(pop) ; 6
(declare-const fvf@75 $FVF<$Seq<$Ref>>)
(push) ; 6
(assert (not (< $Perm.Write (/ (to_real 2) (to_real gsize@3)))))
(check-sat)
; unknown
; 0.02s
(pop) ; 6
(push) ; 6
(assert (not (forall ((x Int) (y Int)) (!
  (implies
    (and
      ($Seq.contains ($Seq.range 0 gsize@3) x)
      ($Seq.contains ($Seq.range 0 gsize@3) y)
      (=
        ($Seq.index ($FVF.lookup_src vs@74 this@1) x)
        ($Seq.index ($FVF.lookup_src vs@74 this@1) y)))
    (= x y))
  :pattern (($Seq.index ($FVF.lookup_src vs@74 this@1) x) ($Seq.index
    ($FVF.lookup_src vs@74 this@1)
    y))))))
(check-sat)
; unsat
; 0.00s
(pop) ; 6
(declare-fun inv@76 ($Ref) Int)
(assert (forall ((r $Ref)) (!
  (implies
    ($Seq.contains ($Seq.range 0 gsize@3) i@73)
    (= ($Seq.index ($FVF.lookup_src vs@74 this@1) (inv@76 r)) r))
  :pattern (($Seq.index ($FVF.lookup_src vs@74 this@1) (inv@76 r))))))
(assert (forall ((i@73 Int)) (!
  (implies
    ($Seq.contains ($Seq.range 0 gsize@3) i@73)
    (= (inv@76 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)) i@73))
  :pattern ((inv@76 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)))
  ; :pattern (($Seq.contains ($Seq.range 0 gsize@3) i@73))
)))
(declare-const vs@77 $FVF<Int>)
(push) ; 6
(assert (not (forall ((r $Ref)) (!
  (=
    (-
      (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
      ($Perm.min
        (ite
          ; (and (<= 0 (inv@76 r)) (< (inv@76 r) gsize@3))
          ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 r))
          (/ (to_real 1) (to_real gsize@3))
          $Perm.No)
        (ite
          (= r ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
          (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
          $Perm.No)))
    $Perm.No)
  ))))
(check-sat)
; unknown
; 0.01s
(pop) ; 6
(push) ; 6
(assert (not (=
  (-
    (ite
      ($Seq.contains
        ($Seq.range 0 gsize@3)
        (inv@76 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)))
      (/ (to_real 1) (to_real gsize@3))
      $Perm.No)
    ($Perm.min
      (ite
        ($Seq.contains
          ($Seq.range 0 gsize@3)
          (inv@76 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)))
        (/ (to_real 1) (to_real gsize@3))
        $Perm.No)
      (ite
        (=
          ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)
          ($Seq.index $t@14 tid@4))
        $Perm.Write
        $Perm.No)))
  $Perm.No)))
(check-sat)
; unknown
(pop) ; 6
(push) ; 6
(assert (not (forall ((r $Ref)) (!
  (=
    (-
      (ite
        ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 r))
        (/ (to_real 1) (to_real gsize@3))
        $Perm.No)
      ($Perm.min
        (-
          (ite
            ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 r))
            (/ (to_real 1) (to_real gsize@3))
            $Perm.No)
          ($Perm.min
            (ite
              ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 r))
              (/ (to_real 1) (to_real gsize@3))
              $Perm.No)
            (ite
              (= r ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
              (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
              $Perm.No)))
        (ite
          (= r ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
          (ite
            ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 r))
            (/ (to_real 1) (to_real gsize@3))
            $Perm.No)
          $Perm.No)))
    $Perm.No)
  ))))
(check-sat)
; unknown
; 0.02s
(pop) ; 6
(push) ; 6
(assert (not (=
  (-
    (-
      (ite
        ($Seq.contains
          ($Seq.range 0 gsize@3)
          (inv@76 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)))
        (/ (to_real 1) (to_real gsize@3))
        $Perm.No)
      ($Perm.min
        (ite
          ($Seq.contains
            ($Seq.range 0 gsize@3)
            (inv@76 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)))
          (/ (to_real 1) (to_real gsize@3))
          $Perm.No)
        (ite
          (=
            ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)
            ($Seq.index $t@14 tid@4))
          $Perm.Write
          $Perm.No)))
    ($Perm.min
      (-
        (ite
          ($Seq.contains
            ($Seq.range 0 gsize@3)
            (inv@76 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)))
          (/ (to_real 1) (to_real gsize@3))
          $Perm.No)
        ($Perm.min
          (ite
            ($Seq.contains
              ($Seq.range 0 gsize@3)
              (inv@76 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)))
            (/ (to_real 1) (to_real gsize@3))
            $Perm.No)
          (ite
            (=
              ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)
              ($Seq.index $t@14 tid@4))
            $Perm.Write
            $Perm.No)))
      (ite
        ($Seq.contains
          ($Seq.range 0 gsize@3)
          (inv@17 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)))
        (/ (to_real 1) (to_real gsize@3))
        $Perm.No)))
  $Perm.No)))
(check-sat)
; unsat
; 0.00s
(pop) ; 6
(assert (forall ((i@73 Int)) (!
  (implies
    (= ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73) ($Seq.index $t@14 tid@4))
    (=
      ($FVF.lookup_Integer_value vs@77 ($Seq.index
        ($FVF.lookup_src vs@74 this@1)
        i@73))
      ($FVF.lookup_Integer_value vs@37 ($Seq.index
        ($FVF.lookup_src vs@74 this@1)
        i@73))))
  :pattern (($FVF.lookup_Integer_value vs@77 ($Seq.index
    ($FVF.lookup_src vs@74 this@1)
    i@73)))
  :pattern (($FVF.lookup_Integer_value vs@37 ($Seq.index
    ($FVF.lookup_src vs@74 this@1)
    i@73))))))
(assert (forall ((i@73 Int)) (!
  (implies
    (ite
      ($Seq.contains
        ($Seq.range 0 gsize@3)
        (inv@17 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73)))
      (< $Perm.No (/ (to_real 1) (to_real gsize@3)))
      false)
    (=
      ($FVF.lookup_Integer_value vs@77 ($Seq.index
        ($FVF.lookup_src vs@74 this@1)
        i@73))
      ($FVF.lookup_Integer_value $t@16 ($Seq.index
        ($FVF.lookup_src vs@74 this@1)
        i@73))))
  :pattern (($FVF.lookup_Integer_value vs@77 ($Seq.index
    ($FVF.lookup_src vs@74 this@1)
    i@73)))
  :pattern (($FVF.lookup_Integer_value $t@16 ($Seq.index
    ($FVF.lookup_src vs@74 this@1)
    i@73))))))
(assert ($Set.equal
  ($FVF.domain_Integer_value vs@77)
  ($Set.union
    ($FVF.domain_Integer_value $t@16)
    ($FVF.domain_Integer_value vs@37))))
; [eval] false || (__last_barrier == 0)
(push) ; 6
(push) ; 7
(assert (not false))
(check-sat)
; unknown
; 0.02s
(pop) ; 7
; (push) ; 7
; ; [then-branch 22] True
; ; [eval] __last_barrier == 0
; (pop) ; 7
; [dead else-branch 22] False
(pop) ; 6
; [eval] __last_barrier == 1
; (push) ; 6
; (assert (not (not (= 0 1))))
; (check-sat)
; ; unsat
; ; 0.00s
; (pop) ; 6
; (push) ; 6
; (assert (not (= 0 1)))
; (check-sat)
; ; unknown
; ; 0.02s
; (pop) ; 6
; [dead then-branch 23] 0 == 1
(push) ; 6
; [else-branch 23] 0 != 1
(assert (not (= 0 1)))
; [eval] __last_barrier == 0
(push) ; 7
(assert (not false))
(check-sat)
; unknown
; 0.02s
(pop) ; 7
(push) ; 7
; [then-branch 24] True
; [eval] this.dst[tid]
(declare-const sk@78 $Ref)
(declare-const vs@79 $FVF<Int>)
(push) ; 8
(assert (not (forall ((r $Ref)) (!
  (=
    (-
      (-
        (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
        ($Perm.min
          (ite
            ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 r))
            (/ (to_real 1) (to_real gsize@3))
            $Perm.No)
          (ite
            (= r ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
            (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
            $Perm.No)))
      ($Perm.min
        (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
        (ite
          (= r ($Seq.index $t@14 tid@4))
          (-
            (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
            ($Perm.min
              (ite
                ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 r))
                (/ (to_real 1) (to_real gsize@3))
                $Perm.No)
              (ite
                (= r ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
                (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
                $Perm.No)))
          $Perm.No)))
    $Perm.No)
  ))))
(check-sat)
; unsat
(pop) ; 8
(push) ; 8
(assert (not (=
  (-
    (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
    ($Perm.min
      (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
      (ite
        (= sk@78 ($Seq.index $t@14 tid@4))
        (-
          (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
          ($Perm.min
            (ite
              ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 sk@78))
              (/ (to_real 1) (to_real gsize@3))
              $Perm.No)
            (ite
              (= sk@78 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
              (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
              $Perm.No)))
        $Perm.No)))
  $Perm.No)))
(check-sat)
; unknown
; 0.04s
(pop) ; 8
(push) ; 8
(assert (not (forall ((r $Ref)) (!
  (=
    (-
      (-
        (ite
          ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 r))
          (/ (to_real 1) (to_real gsize@3))
          $Perm.No)
        ($Perm.min
          (-
            (ite
              ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 r))
              (/ (to_real 1) (to_real gsize@3))
              $Perm.No)
            ($Perm.min
              (ite
                ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 r))
                (/ (to_real 1) (to_real gsize@3))
                $Perm.No)
              (ite
                (= r ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
                (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
                $Perm.No)))
          (ite
            (= r ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
            (ite
              ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 r))
              (/ (to_real 1) (to_real gsize@3))
              $Perm.No)
            $Perm.No)))
      ($Perm.min
        (-
          (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
          ($Perm.min
            (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
            (ite
              (= r ($Seq.index $t@14 tid@4))
              (-
                (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
                ($Perm.min
                  (ite
                    ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 r))
                    (/ (to_real 1) (to_real gsize@3))
                    $Perm.No)
                  (ite
                    (= r ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
                    (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
                    $Perm.No)))
              $Perm.No)))
        (ite
          (= r ($Seq.index $t@14 tid@4))
          (-
            (ite
              ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 r))
              (/ (to_real 1) (to_real gsize@3))
              $Perm.No)
            ($Perm.min
              (-
                (ite
                  ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 r))
                  (/ (to_real 1) (to_real gsize@3))
                  $Perm.No)
                ($Perm.min
                  (ite
                    ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 r))
                    (/ (to_real 1) (to_real gsize@3))
                    $Perm.No)
                  (ite
                    (= r ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
                    (ite (= r ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
                    $Perm.No)))
              (ite
                (= r ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
                (ite
                  ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 r))
                  (/ (to_real 1) (to_real gsize@3))
                  $Perm.No)
                $Perm.No)))
          $Perm.No)))
    $Perm.No)
  ))))
(check-sat)
; unknown
; 0.03s
(pop) ; 8
(push) ; 8
(assert (not (=
  (-
    (-
      (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
      ($Perm.min
        (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
        (ite
          (= sk@78 ($Seq.index $t@14 tid@4))
          (-
            (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
            ($Perm.min
              (ite
                ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 sk@78))
                (/ (to_real 1) (to_real gsize@3))
                $Perm.No)
              (ite
                (= sk@78 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
                (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
                $Perm.No)))
          $Perm.No)))
    ($Perm.min
      (-
        (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
        ($Perm.min
          (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
          (ite
            (= sk@78 ($Seq.index $t@14 tid@4))
            (-
              (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
              ($Perm.min
                (ite
                  ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 sk@78))
                  (/ (to_real 1) (to_real gsize@3))
                  $Perm.No)
                (ite
                  (= sk@78 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
                  (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
                  $Perm.No)))
            $Perm.No)))
      (ite
        (= sk@78 ($Seq.index $t@14 tid@4))
        (-
          (ite
            ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 sk@78))
            (/ (to_real 1) (to_real gsize@3))
            $Perm.No)
          ($Perm.min
            (-
              (ite
                ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 sk@78))
                (/ (to_real 1) (to_real gsize@3))
                $Perm.No)
              ($Perm.min
                (ite
                  ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 sk@78))
                  (/ (to_real 1) (to_real gsize@3))
                  $Perm.No)
                (ite
                  (= sk@78 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
                  (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
                  $Perm.No)))
            (ite
              (= sk@78 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
              (ite
                ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 sk@78))
                (/ (to_real 1) (to_real gsize@3))
                $Perm.No)
              $Perm.No)))
        $Perm.No)))
  $Perm.No)))
(check-sat)
; unsat
(pop) ; 8
(assert (forall ((sk@78 $Ref)) (!
  (implies
    (<
      $Perm.No
      (-
        (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
        ($Perm.min
          (ite
            ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 sk@78))
            (/ (to_real 1) (to_real gsize@3))
            $Perm.No)
          (ite
            (= sk@78 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
            (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
            $Perm.No))))
    (=
      ($FVF.lookup_Integer_value vs@79 sk@78)
      ($FVF.lookup_Integer_value vs@37 sk@78)))
  :pattern (($FVF.lookup_Integer_value vs@79 sk@78))
  :pattern (($FVF.lookup_Integer_value vs@37 sk@78)))))
(assert (forall ((sk@78 $Ref)) (!
  (implies
    (<
      $Perm.No
      (-
        (ite
          ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 sk@78))
          (/ (to_real 1) (to_real gsize@3))
          $Perm.No)
        ($Perm.min
          (-
            (ite
              ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 sk@78))
              (/ (to_real 1) (to_real gsize@3))
              $Perm.No)
            ($Perm.min
              (ite
                ($Seq.contains ($Seq.range 0 gsize@3) (inv@76 sk@78))
                (/ (to_real 1) (to_real gsize@3))
                $Perm.No)
              (ite
                (= sk@78 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
                (ite (= sk@78 ($Seq.index $t@14 tid@4)) $Perm.Write $Perm.No)
                $Perm.No)))
          (ite
            (= sk@78 ($Seq.index ($FVF.lookup_src vs@74 this@1) i@73))
            (ite
              ($Seq.contains ($Seq.range 0 gsize@3) (inv@17 sk@78))
              (/ (to_real 1) (to_real gsize@3))
              $Perm.No)
            $Perm.No))))
    (=
      ($FVF.lookup_Integer_value vs@79 sk@78)
      ($FVF.lookup_Integer_value $t@16 sk@78)))
  :pattern (($FVF.lookup_Integer_value vs@79 sk@78))
  :pattern (($FVF.lookup_Integer_value $t@16 sk@78)))))
(assert ($Set.equal
  ($FVF.domain_Integer_value vs@79)
  ($Set.union
    ($FVF.domain_Integer_value $t@16)
    ($FVF.domain_Integer_value vs@37))))
; [eval] (0 <= k) && (k <= half)
; [eval] 0 <= k
(push) ; 8
(push) ; 9
(assert (not false))
(echo "This might take a while. Or not.")
(check-sat)
; unknown
; 0.11s
(pop) ; 9

(get-info :all-statistics)