Function FreshReal

lean_py/z3/core.py:2172–2176

Create a fresh real constant.

(prefix: str = "x")

def FreshReal(prefix: str = "x") -> ArithRef:
    """Create a fresh real constant."""
    r = FreshConst(RealSort(), prefix)
    assert isinstance(r, ArithRef)
    return r


# ---------------------------------------------------------------------------