The back pred files have been eliminated. The small backpred string is now directly included in ProverInterface.cs.

2 files changed, 0 insertions, 139 deletions

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)