Guide: push/pop for incremental solving.
(self, kernel)
| 851 | assert s.check() == sat |
| 852 | |
| 853 | def test_solver_push_pop(self, kernel): |
| 854 | """Guide: push/pop for incremental solving.""" |
| 855 | x = Int("x") |
| 856 | s = Solver() |
| 857 | s.add(x > 0) |
| 858 | s.push() |
| 859 | s.add(x < 0) |
| 860 | assert s.check() == unsat |
| 861 | s.pop() |
| 862 | # Only x > 0 remains: not contradictory |
| 863 | assert s.check() != unsat |
| 864 | |
| 865 | def test_solver_nested_push_pop(self, kernel): |
| 866 | """Multiple push/pop levels.""" |