From 554fb3a6780c412b81dc935835c2760e4cbe0b4d Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 10 Aug 2010 02:16:29 +0000
Subject: Boogie: Added boolean code expressions (sans well-formedness checks
 on the input).

---
 Binaries/TypedUnivBackPred2.sx | 4 ++++
 Binaries/UnivBackPred2.sx      | 2 ++
 2 files changed, 6 insertions(+)

(limited to 'Binaries')

diff --git a/Binaries/TypedUnivBackPred2.sx b/Binaries/TypedUnivBackPred2.sx
index 5ee200f1..450e658a 100644
--- a/Binaries/TypedUnivBackPred2.sx
+++ b/Binaries/TypedUnivBackPred2.sx
@@ -10,6 +10,8 @@
 (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
@@ -126,6 +128,8 @@
   ; 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
 ; -------------------------------------------------------------------------
diff --git a/Binaries/UnivBackPred2.sx b/Binaries/UnivBackPred2.sx
index 7c3dac8e..7e30017b 100644
--- a/Binaries/UnivBackPred2.sx
+++ b/Binaries/UnivBackPred2.sx
@@ -80,6 +80,8 @@
   ; Reflect plus
   (FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b)))
 
+  (EQ (tickleBool |@false|) |@true|)
+  (EQ (tickleBool |@true|) |@true|)
 ))  ;; AND, BG_PUSH
 ; End Boogie universal background predicate
 ; -------------------------------------------------------------------------
-- 
cgit v1.2.3