encodings: fixed hey_const

moves-rwth · Jan 23, 2024 · d28c5c6 · d28c5c6
1 parent 068757a
commit d28c5c6
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 7 deletions.
diff --git a/src/proof_rules/tests.rs b/src/proof_rules/tests.rs
@@ -158,7 +158,7 @@ fn test_ost_transform() {
                     k = (k + 1)
                     tick cast(EUReal, 1)
                     coassert (cast(EUReal, 2) * [a])
-                    coassume cast(EUReal, 0)
+                    coassume ∞
                 } else {
             
                 }
@@ -213,7 +213,7 @@ fn test_ost_transform() {
                     if prob_choice { a = false } else { b = (b + 1) }
                     k = (k + 1)
                     coassert (cast(EUReal, b) + [a])
-                    coassume cast(EUReal, 0)
+                    coassume ∞
                 } else {
             
                 }
@@ -301,7 +301,7 @@ fn test_past_transform() {
                 if (1 <= x) {
                     x = (x - 1)
                     coassert cast(EUReal, (x + 1))
-                    coassume cast(EUReal, 0)
+                    coassume ∞
                 } else {
             
                 }

diff --git a/src/proof_rules/util.rs b/src/proof_rules/util.rs
@@ -87,12 +87,13 @@ pub fn encode_iter(span: Span, stmt: &Stmt, next_iter: Vec<Stmt>) -> Option<Stmt
 /// Constant program which always evaluates to the given expression
 pub fn hey_const(span: Span, expr: &Expr, direction: Direction, tcx: &TyCtx) -> Vec<Stmt> {
     let builder = ExprBuilder::new(span);
+    let extrem_lit = match direction {
+        Direction::Up => builder.top_lit(tcx.spec_ty()),
+        Direction::Down => builder.bot_lit(tcx.spec_ty()),
+    };
     vec![
         Spanned::new(span, StmtKind::Assert(direction, expr.clone())),
-        Spanned::new(
-            span,
-            StmtKind::Assume(direction, builder.bot_lit(tcx.spec_ty())),
-        ),
+        Spanned::new(span, StmtKind::Assume(direction, extrem_lit)),
     ]
 }