diff options
| author |  rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
| commit | 554fb3a6780c412b81dc935835c2760e4cbe0b4d (patch) | |
| tree | b50aa3dbbb369a52751bfcb9f142c9c928e591ae /Binaries/UnivBackPred2.sx | |
| parent | c2aa0b56fce36a101c3bef7ce901b8f26dcb5f08 (diff) | |
Boogie: Added boolean code expressions (sans well-formedness checks on the input).
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
; -------------------------------------------------------------------------
|