Method test_push_pop_restores

tests/test_z3_semantic.py:1076–1084

(self, kernel)

        assert s.check() == unsat

    def test_push_pop_restores(self, kernel):
        s = Solver()
        s.add(BoolVal(True))
        s.push()
        s.add(BoolVal(False))
        assert s.check() == unsat
        s.pop()
        # After pop, only True remains — provable, so sat
        assert s.check() == sat

    def test_nested_push_pop(self, kernel):
        x = Int("x")