diff options
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/TypedUnivBackPred2.sx | 4 | ||||
| -rw-r--r-- | Binaries/UnivBackPred2.sx | 2 |
2 files changed, 6 insertions, 0 deletions
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
; -------------------------------------------------------------------------
|