(self, kernel)
| 435 | assert s.check() == unsat |
| 436 | |
| 437 | def test_push_pop(self, kernel): |
| 438 | x = Int("x") |
| 439 | s = Solver() |
| 440 | s.add(x > 0) |
| 441 | s.push() |
| 442 | s.add(x < 0) |
| 443 | assert s.check() == unsat |
| 444 | s.pop() |
| 445 | # After pop, only x > 0 remains -- not contradictory |
| 446 | assert s.check() == unknown |
| 447 | |
| 448 | def test_context_manager(self, kernel): |
| 449 | x = Int("x") |