Multiple push/pop levels.
(self, kernel)
| 863 | assert s.check() != unsat |
| 864 | |
| 865 | def test_solver_nested_push_pop(self, kernel): |
| 866 | """Multiple push/pop levels.""" |
| 867 | x = Int("x") |
| 868 | s = Solver() |
| 869 | s.add(x > 0) |
| 870 | s.push() |
| 871 | s.add(x > 5) |
| 872 | s.push() |
| 873 | s.add(x < 3) |
| 874 | assert s.check() == unsat # x > 5 and x < 3 |
| 875 | s.pop() |
| 876 | # x > 0 and x > 5: not contradictory |
| 877 | assert s.check() != unsat |
| 878 | s.pop() |
| 879 | # Just x > 0: not contradictory |
| 880 | assert s.check() != unsat |
| 881 | |
| 882 | def test_solver_assertions(self, kernel): |
| 883 | """Guide: solver.assertions() returns added constraints.""" |