From dcc75c6fd59360f4e94d46691988d0c9e56c8278 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Sun, 3 Jan 2016 18:30:03 +0100
Subject: [PATCH] Ignore assertion in GenC phase
---
src/main/scala/leon/genc/CConverter.scala | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala
index 596bef698..10408436e 100644
--- a/src/main/scala/leon/genc/CConverter.scala
+++ b/src/main/scala/leon/genc/CConverter.scala
@@ -402,8 +402,9 @@ class CConverter(val ctx: LeonContext, val prog: Program) {
case BVLShiftRight(lhs, rhs) => fatalError("operator >>> not supported")
// Ignore assertions for now
- case Ensuring(body, _) => convert(body)
- case Require(_, body) => convert(body)
+ case Ensuring(body, _) => convert(body)
+ case Require(_, body) => convert(body)
+ case Assert(_, _, body) => convert(body)
case IfExpr(cond1, thn1, elze1) =>
val condF = convertAndFlatten(cond1)
--
GitLab