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