1 files changed, 131 insertions, 0 deletions
diff --git a/Binaries/UnivBackPred2.smt b/Binaries/UnivBackPred2.smt
new file mode 100644
index 00000000..76c77d60
--- /dev/null
+++ b/Binaries/UnivBackPred2.smt
@@ -0,0 +1,131 @@
+; -------------------------------------------------------------------------
+; 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
+; -------------------------------------------------------------------------
+