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 index 8cf7a872a..6887bbb06 100644 --- 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 index 22c8c3e31..1992afe76 100644 --- 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(