Method test_solver_context_manager

tests/test_z3_ported.py:898–906

With statement for push/pop.

(self, kernel)

        assert len(s.assertions()) == 0

    def test_solver_context_manager(self, kernel):
        """With statement for push/pop."""
        s = Solver()
        x = Int("x")
        s.add(x > 0)
        with s:
            s.add(x < 0)
            assert s.check() == unsat
        assert len(s.assertions()) == 1

    def test_model_not_supported(self, kernel):
        """model() raises since Lean is not an SMT solver."""