From 57f3b0868aa862a718b6703679f26d8ff148eb1f Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sun, 8 Dec 2013 22:30:52 -0800
Subject: The back pred files have been eliminated.  The small backpred string
 is now directly included in ProverInterface.cs.

---
 Binaries/UnivBackPred2.smt  | 131 --------------------------------------------
 Binaries/UnivBackPred2.smt2 |   8 ---
 2 files changed, 139 deletions(-)
 delete mode 100644 Binaries/UnivBackPred2.smt
 delete mode 100644 Binaries/UnivBackPred2.smt2

(limited to 'Binaries')

diff --git a/Binaries/UnivBackPred2.smt b/Binaries/UnivBackPred2.smt
deleted file mode 100644
index 76c77d60..00000000
--- a/Binaries/UnivBackPred2.smt
+++ /dev/null
@@ -1,131 +0,0 @@
-; -------------------------------------------------------------------------
-; Boogie universal background predicate
-; Copyright (c) 2004-2006, Microsoft Corp.
-  :logic AUFLIA
-  :category { industrial }
-
-:extrasorts ( boogieU )
-:extrasorts ( boogieT )
-:extrasorts ( TermBool )
-
-:extrafuns (( boolTrue TermBool ))
-:extrafuns (( boolFalse TermBool ))
-:extrafuns (( boolIff TermBool TermBool TermBool ))
-:extrafuns (( boolImplies TermBool TermBool TermBool ))
-:extrafuns (( boolAnd TermBool TermBool TermBool ))
-:extrafuns (( boolOr TermBool TermBool TermBool ))
-:extrafuns (( boolNot TermBool TermBool ))
-:extrafuns (( UEqual boogieU boogieU TermBool ))
-:extrafuns (( TEqual boogieT boogieT TermBool ))
-:extrafuns (( IntEqual Int Int TermBool ))
-:extrafuns (( intLess Int Int TermBool ))
-:extrafuns (( intAtMost Int Int TermBool ))
-:extrafuns (( intGreater Int Int TermBool ))
-:extrafuns (( intAtLeast Int Int TermBool ))
-:extrafuns (( boogieIntMod Int Int Int ))
-:extrafuns (( boogieIntDiv Int Int Int ))
-
-; used for translation with type premisses
-:extrapreds (( UOrdering2 boogieU boogieU ))
-; used for translation with type arguments
-:extrapreds (( UOrdering3 boogieT boogieU boogieU ))
-
-; used for translation with type premisses
-:extrafuns (( TermUOrdering2 boogieU boogieU TermBool ))
-; used for translation with type arguments
-:extrafuns (( TermUOrdering3 boogieT boogieU boogieU TermBool ))
-
-  ; formula/term axioms
-  :assumption
-  (forall (?x TermBool) (?y TermBool)
-    (iff
-      (= (boolIff ?x ?y) boolTrue)
-      (iff (= ?x boolTrue) (= ?y boolTrue))))
-
-  :assumption
-  (forall (?x TermBool) (?y TermBool)
-    (iff
-      (= (boolImplies ?x ?y) boolTrue)
-      (implies (= ?x boolTrue) (= ?y boolTrue))))
-
-  :assumption
-  (forall (?x TermBool) (?y TermBool)
-    (iff
-      (= (boolAnd ?x ?y) boolTrue)
-      (and (= ?x boolTrue) (= ?y boolTrue))))
-
-  :assumption
-  (forall (?x TermBool) (?y TermBool)
-    (iff
-      (= (boolOr ?x ?y) boolTrue)
-      (or (= ?x boolTrue) (= ?y boolTrue))))
-
-  :assumption
-  (forall (?x TermBool)
-    (iff
-      (= (boolNot ?x) boolTrue)
-      (not (= ?x boolTrue)))
-    :pat { (boolNot ?x) }
-  )
-
-  :assumption
-  (forall (?x boogieU) (?y boogieU)
-    (iff
-      (= (UEqual ?x ?y) boolTrue)
-      (= ?x ?y)))
-
-  :assumption
-  (forall (?x boogieT) (?y boogieT)
-    (iff
-      (= (TEqual ?x ?y) boolTrue)
-      (= ?x ?y)))
-
-  :assumption
-  (forall (?x Int) (?y Int)
-    (iff
-      (= (IntEqual ?x ?y) boolTrue)
-      (= ?x ?y)))
-
-  :assumption
-  (forall (?x Int) (?y Int)
-    (iff
-      (= (intLess ?x ?y) boolTrue)
-      (< ?x ?y)))
-
-  :assumption
-  (forall (?x Int) (?y Int)
-    (iff
-      (= (intAtMost ?x ?y) boolTrue)
-      (<= ?x ?y)))
-
-  :assumption
-  (forall (?x Int) (?y Int)
-    (iff
-      (= (intAtLeast ?x ?y) boolTrue)
-      (>= ?x ?y)))
-
-  :assumption
-  (forall (?x Int) (?y Int)
-    (iff
-      (= (intGreater ?x ?y) boolTrue)
-      (> ?x ?y)))
-
-  ; false is not true
-  :assumption
-  (distinct boolFalse boolTrue)
-
-  :assumption
-  (forall (?x boogieU) (?y boogieU)
-    (iff
-      (= (TermUOrdering2 ?x ?y) boolTrue)
-      (UOrdering2 ?x ?y)))
-
-  :assumption
-  (forall (?x boogieT) (?y boogieU) (?z boogieU)
-    (iff
-      (= (TermUOrdering3 ?x ?y ?z) boolTrue)
-      (UOrdering3 ?x ?y ?z)))
-
-; End Boogie universal background predicate
-; -------------------------------------------------------------------------
-
diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2
deleted file mode 100644
index 9bb05bfb..00000000
--- a/Binaries/UnivBackPred2.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; Boogie universal background predicate
-; Copyright (c) 2004-2010, Microsoft Corp.
-(set-info :category "industrial")
-(declare-sort |T@U| 0)
-(declare-sort |T@T| 0)
-(declare-fun real_pow (Real Real) Real)
-(declare-fun UOrdering2 (|T@U| |T@U|) Bool)
-(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)
-- 
cgit v1.2.3