catch ugly exception when z3 java api not in path

viperproject · Sep 8, 2023 · fda5d54 · fda5d54
1 parent 7b52085
commit fda5d54
Showing 1 changed file with 19 additions and 11 deletions.
diff --git a/src/main/scala/viper/gobra/backend/Silicon.scala b/src/main/scala/viper/gobra/backend/Silicon.scala
@@ -11,7 +11,6 @@ import viper.silicon
 import viper.silver.ast.Program
 import viper.silver.reporter._
 import viper.silver.verifier.{Failure, Success, VerificationResult}
-
 import scala.concurrent.Future
 
 class Silicon(commandLineArguments: Seq[String]) extends ViperVerifier {
@@ -23,18 +22,27 @@ class Silicon(commandLineArguments: Seq[String]) extends ViperVerifier {
       val backend: silicon.Silicon = silicon.Silicon.fromPartialCommandLineArguments(commandLineArguments, reporter)
 
       val startTime = System.currentTimeMillis()
-      backend.start()
-      val result = backend.verify(program)
-      backend.stop()
+      try {
+        backend.start()
+        val result = backend.verify(program)
+        backend.stop()
 
-      result match {
-        case Success =>
-          reporter report OverallSuccessMessage(backend.name, System.currentTimeMillis() - startTime)
-        case f@Failure(_) =>
-          reporter report OverallFailureMessage(backend.name, System.currentTimeMillis() - startTime, f)
-      }
+        result match {
+          case Success =>
+            reporter report OverallSuccessMessage(backend.name, System.currentTimeMillis() - startTime)
+          case f@Failure(_) =>
+            reporter report OverallFailureMessage(backend.name, System.currentTimeMillis() - startTime, f)
+        }
 
-      result
+        result
+      } catch {
+        case _: java.lang.UnsatisfiedLinkError => println("Couldn't find Z3 java API. No libz3java in java.library.path")
+          new Failure(Seq.empty)
+        case e: Throwable =>
+          println("Couldn't verify package due to internal error:")
+          println(e.getMessage())
+          new Failure(Seq.empty)
+      }
     }
   }
 }