Method test_model_not_supported

tests/test_z3_ported.py:908–912

model() raises since Lean is not an SMT solver.

(self, kernel)

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

    def test_model_not_supported(self, kernel):
        """model() raises since Lean is not an SMT solver."""
        s = Solver()
        with pytest.raises(NotImplementedError):
            s.model()


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