Guide: create, add, check.
(self, kernel)
| 838 | """From z3py guide: Solver push/pop, assertions, model stub.""" |
| 839 | |
| 840 | def test_solver_basic(self, kernel): |
| 841 | """Guide: create, add, check.""" |
| 842 | s = Solver() |
| 843 | x = Int("x") |
| 844 | s.add(x > 10) |
| 845 | s.add(x < 5) |
| 846 | assert s.check() == unsat |
| 847 | |
| 848 | def test_solver_satisfiable_empty(self, kernel): |
| 849 | """Empty solver is sat.""" |