diff --git a/kdrag/solvers/__init__.py b/kdrag/solvers/__init__.py index 08a5112..53b783a 100644 --- a/kdrag/solvers/__init__.py +++ b/kdrag/solvers/__init__.py @@ -420,7 +420,6 @@ class MultiSolver(BaseSolver): solver_classes = [ VampireTHFSolver, EProverTHFSolver, - ZipperpositionSolver, LeoIIISolver, ] if shutil.which("zipperposition") is not None: diff --git a/tests/test_solver.py b/tests/test_solver.py index ded1a23..2b6b831 100644 --- a/tests/test_solver.py +++ b/tests/test_solver.py @@ -203,7 +203,8 @@ def check(s): assert check(VampireTHFSolver()) == smt.unsat assert check(EProverTHFSolver()) == smt.unsat assert check(MultiSolver()) == smt.unsat - assert check(ZipperpositionSolver()) == smt.unsat + if shutil.which("zipperposition") is not None: + assert check(ZipperpositionSolver()) == smt.unsat assert check(smt.Solver()) == smt.unsat assert check(solvers.VampireSolver()) == smt.unsat