fix z3 and boolector

vorpal-research · Nov 1, 2023 · 3b4db26 · 3b4db26
1 parent 2f96412
commit 3b4db26
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/kex-boolector/src/main/kotlin/org/vorpal/research/kex/smt/boolector/BoolectorSolver.kt b/kex-boolector/src/main/kotlin/org/vorpal/research/kex/smt/boolector/BoolectorSolver.kt
@@ -73,7 +73,7 @@ class BoolectorSolver(
         val result = check(boolectorState, boolectorQuery)
         log.debug("Check finished")
         return when (result) {
-            Btor.Status.UNSAT -> Result.UnsatResult
+            Btor.Status.UNSAT -> Result.UnsatResult()
             Btor.Status.UNKNOWN -> Result.UnknownResult("should not happen")
             Btor.Status.SAT -> Result.SatResult(collectModel(ctx, state))
         }

diff --git a/kex-z3/src/main/kotlin/org/vorpal/research/kex/smt/z3/Z3Solver.kt b/kex-z3/src/main/kotlin/org/vorpal/research/kex/smt/z3/Z3Solver.kt
@@ -68,7 +68,7 @@ class Z3Solver(
         val result = check(z3State, queryBuilder(z3query))
         log.debug("Check finished")
         return when (result.first) {
-            Status.UNSATISFIABLE -> Result.UnsatResult
+            Status.UNSATISFIABLE -> Result.UnsatResult()
             Status.UNKNOWN -> Result.UnknownResult(result.second as String)
             Status.SATISFIABLE -> Result.SatResult(collectModel(ctx, result.second as Model, state))
         }
@@ -489,7 +489,7 @@ class Z3Solver(
         log.debug("Check finished")
         return results.mapIndexed { index, (status, any) ->
             when (status) {
-                Status.UNSATISFIABLE -> Result.UnsatResult
+                Status.UNSATISFIABLE -> Result.UnsatResult()
                 Status.UNKNOWN -> Result.UnknownResult(any as String)
                 Status.SATISFIABLE -> Result.SatResult(
                     collectModel(