Create a fresh integer constant.
(prefix: str = "x")
| 2156 | |
| 2157 | |
| 2158 | def FreshInt(prefix: str = "x") -> ArithRef: |
| 2159 | """Create a fresh integer constant.""" |
| 2160 | r = FreshConst(IntSort(), prefix) |
| 2161 | assert isinstance(r, ArithRef) |
| 2162 | return r |
| 2163 | |
| 2164 | |
| 2165 | def FreshBool(prefix: str = "b") -> BoolRef: |