1 files changed, 0 insertions, 135 deletions
diff --git a/Binaries/TypedUnivBackPred2.sx b/Binaries/TypedUnivBackPred2.sx
deleted file mode 100644
index 450e658a..00000000
--- a/Binaries/TypedUnivBackPred2.sx
+++ /dev/null
@@ -1,135 +0,0 @@
-; -------------------------------------------------------------------------
-; Boogie 2 universal background predicate for Z3 (Simplify notation with types)
-; Copyright (c) 2004-2009, Microsoft Corp.
-
-(DEFTYPE $int :BUILTIN Int)
-(DEFTYPE $bool :BUILTIN bool)
-(DEFTYPE U)
-(DEFTYPE T)
-
-(DEFOP <: U U $bool)         ; used for translation with type premisses
-(DEFOP <:: T U U $bool)      ; used for translation with type arguments
-
-(DEFOP tickleBool $bool $bool) ; used in triggers to exhaustively instantiate quantifiers over booleans
-
-(BG_PUSH (AND
-
-  ; false is not true
-
-  (DISTINCT |@false| |@true|)
-
-  ; we assume type correctness of the operations here
-  ; a-l>=0 ==> (v ++ w:l)[a:b] = v[a-l:b-l]
-  (FORALL (v lv w lw lvw a b)
-    (QID bv:e:c1)
-    (PATS ($bv_extract ($bv_concat v lv w lw) lvw a b))
-    (IMPLIES
-      (>= (- a lw) 0)
-      (EQ ($bv_extract ($bv_concat v lv w lw) lvw a b) ($bv_extract v lv (- a lw) (- b lw)))))
-
-  ; b<=l ==> (v ++ w:l)[a:b] = w[a:b]
-  (FORALL (v lv w lw lvw a b)
-    (QID bv:e:c2)
-    (PATS ($bv_extract ($bv_concat v lv w lw) lvw a b))
-    (IMPLIES
-      (<= b lw)
-      (EQ ($bv_extract ($bv_concat v lv w lw) lvw a b) ($bv_extract w lw a b))))
-
-  ; v:l
-  ; a>=x || b<=y ==> (v[x:l] ++ w ++ v[0:y])[a:b] = v[a:b]
-  (FORALL (v lv x lxv w lw lwy y a b)
-    (QID bv:e:c3)
-    (PATS 
-      ($bv_extract 
-        ($bv_concat 
-          ($bv_extract v lv x lv) lxv
-	  ($bv_concat 
-	    w lw
-            ($bv_extract v lv 0 y) y) lwy) lv a b))
-    (IMPLIES
-      (AND
-        (EQ lw (- x y))
-        (EQ lxv (- lv x))
-        (EQ lwy (+ w y))
-        (OR (>= a x) (<= b y)))
-      (EQ
-        ($bv_extract 
-          ($bv_concat 
-            ($bv_extract v lv x lv) lxv
-	    ($bv_concat 
-	      w lw
-              ($bv_extract v lv 0 y) y) lwy) lv a b)
-	($bv_extract v lv a b))))
-
-  ; a>=x ==> (v[x:l] ++ w)[a:b] = v[a:b]
-  (FORALL (v lv x lxv w a b)
-    (QID bv:e:c4)
-    (PATS 
-      ($bv_extract 
-        ($bv_concat 
-          ($bv_extract v lv x lv) lxv 
-	  w x) 
-	lv a b))
-    (IMPLIES
-      (AND
-        (EQ lxv (- lv x))
-        (>= a x))
-      (EQ
-        ($bv_extract 
-          ($bv_concat 
-            ($bv_extract v lv x lv) lxv 
-	    w x) 
-	  lv a b)
-	($bv_extract v lv a b))))
-
-  (FORALL (v l)
-    (QID bv:e:0)
-    (PATS ($bv_extract v l 0 l))
-      (EQ ($bv_extract v l 0 l) v))
-
-  (FORALL (n)
-    (QID bv:pow)
-    (PATS ($pow2 n))
-      (IMPLIES (> n 0) (EQ ($pow2 n) (* 2 ($pow2 (- n 1))))))
-
-  (EQ ($pow2 0) 1)
-
-  ; 0 <= v < 2^Y ==> 0bvX ++ v[0:Y] == v
-  (FORALL (v l a b)
-    (QID bv:e:pow)
-    (PATS ($bv_concat 0 b ($bv_extract v l 0 a) a))
-    (IMPLIES
-      (AND
-        (<= 0 v)
-        (< v ($pow2 a))
-        (EQ l (+ a b)))
-      (EQ ($bv_concat 0 b ($bv_extract v l 0 a) a) v)))
-  
-  ; X > 0 ==> 0bvX ++ v >= 0
-  (FORALL (v a b)
-    (QID bv:e:pos)
-    (PATS ($bv_concat 0 b v a))
-    (IMPLIES
-      (> b 0)
-      (>= ($bv_concat 0 b v a) 0)))
-
-  ;; unsound?
-;  (FORALL (lv w lw)
-;    (QID bv:c:0)
-;    (PATS ($bv_concat 0 lv w lw))
-;    (EQ ($bv_concat 0 lv w lw) w))
-  ;; matching loop
-;  (FORALL (v l1 a b l2 c d)
-;    (QID bv:e:e)
-;    (PATS ($bv_extract ($bv_extract v l1 a b) l2 c d))
-;    (EQ ($bv_extract ($bv_extract v l1 a b) l2 c d) ($bv_extract v l1 (+ c a) (+ d a))))
-  
-
-  ; Reflect plus
-  (FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b)))
-
-  (tickleBool FALSE)
-  (tickleBool TRUE)
-))  ;; AND, BG_PUSH
-; End Boogie universal background predicate
-; -------------------------------------------------------------------------