Method test_tactic_solver

tests/test_z3_ported.py:2759–2765

(self, kernel)

        assert t2 is t

    def test_tactic_solver(self, kernel):
        t = Tactic("grind")
        s = t.solver()
        assert isinstance(s, Solver)
        x = Int("x")
        s.add(x > 0, x < 0)
        assert s.check() == unsat


# ===================================================================