bug

viperproject · Sep 12, 2023 · 2acade4 · 2acade4
1 parent e83b7b8
commit 2acade4
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala
@@ -186,9 +186,9 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
     // TODO: Check consistency of cfgs.
     //val consistencyErrors = utils.consistency.check(program)
 
-    if (consistencyErrors.nonEmpty) {
-      SilFailure(consistencyErrors)
-    } else {
+    //if (consistencyErrors.nonEmpty) {
+    //  SilFailure(consistencyErrors)
+    //} else {
       var result: Option[SilVerificationResult] = None
       val executor = Executors.newSingleThreadExecutor()
 
@@ -232,7 +232,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)]
 
       assert(result.nonEmpty, "The result of the verification run wasn't stored appropriately")
       result.get
-    }
+    //}
   }
 
   private def runVerifier(program: ast.Program, cfgs: Seq[SilverCfg], inputFile: Option[String]): List[Failure] = {