More meaningful error message for smtlib error

ftsrg · Jan 7, 2024 · 4dcde47 · 4dcde47
1 parent be2e4e8
commit 4dcde47
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 3 deletions.
diff --git a/.github/actions/benchexec-test/theta.xml b/.github/actions/benchexec-test/theta.xml
@@ -9,7 +9,7 @@
     <option name="--disable-arg-generation"/>
     <option name="--backend">PORTFOLIO</option>
     <option name="--portfolio">COMPLEX</option>
-    <option name="--loglevel">RESULT</option>
+    <option name="--loglevel">INFO</option>
 
     <rundefinition name="SV-COMP24_unreach-call">
         <tasks name="ReachSafety-Arrays">

diff --git a/.../src/main/java/hu/bme/mit/theta/solver/smtlib/solver/installer/SmtLibSolverInstaller.java b/.../src/main/java/hu/bme/mit/theta/solver/smtlib/solver/installer/SmtLibSolverInstaller.java
@@ -191,7 +191,8 @@ public final SolverFactory getSolverFactory(final Path home, final String versio
 
             final var installDir = home.resolve(version);
             if (!Files.exists(installDir)) {
-                throw new SmtLibSolverInstallerException("The version is not installed");
+                throw new SmtLibSolverInstallerException("The version <" + version
+                        + "> is not installed in <" + home + ">");
             }
 
             try {

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
@@ -83,7 +83,13 @@ data class InputConfig(
 
     @Parameter(names = ["--property-value"], description = "Property")
     var property: ErrorDetection = ErrorDetection.ERROR_LOCATION
-) : Config
+) : Config {
+
+    override fun toString(): String {
+        return "InputConfig(inputFile=${input}, catFile=${catFile}, parseCtx=${parseCtx}, " +
+            "xcfaWCtx=${xcfaWCtx?.let { "present" } ?: "missing"}, propertyFile=${propertyFile}, property=${property}"
+    }
+}
 
 interface SpecFrontendConfig : Config
 data class FrontendConfig<T : SpecFrontendConfig>(

diff --git a/...rojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/SolverRegistration.kt b/...rojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/SolverRegistration.kt
@@ -35,9 +35,11 @@ fun registerAllSolverManagers(home: String, logger: Logger) {
     SolverManager.closeAll()
     // register solver managers
     SolverManager.registerSolverManager(Z3SolverManager.create())
+    logger.write(Logger.Level.INFO, "Registered Z3 SolverManager")
     if (OsHelper.getOs() == OsHelper.OperatingSystem.LINUX) {
         val homePath = Path.of(home)
         val smtLibSolverManager: SmtLibSolverManager = SmtLibSolverManager.create(homePath, logger)
         SolverManager.registerSolverManager(smtLibSolverManager)
+        logger.write(Logger.Level.INFO, "Registered SMT-LIB SolverManager")
     }
 }