(self, kernel)
| 1084 | assert s.check() == sat |
| 1085 | |
| 1086 | def test_nested_push_pop(self, kernel): |
| 1087 | x = Int("x") |
| 1088 | s = Solver() |
| 1089 | s.add(x == x) # tautology |
| 1090 | s.push() |
| 1091 | s.add(IntVal(1) == IntVal(1)) # tautology |
| 1092 | s.push() |
| 1093 | s.add(IntVal(1) == IntVal(2)) # contradiction |
| 1094 | assert s.check() == unsat |
| 1095 | s.pop() |
| 1096 | assert s.check() == sat # x == x ∧ 1 == 1 |
| 1097 | s.pop() |
| 1098 | assert s.check() == sat # x == x |
| 1099 | |
| 1100 | def test_reset_clears(self, kernel): |
| 1101 | s = Solver() |