MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / test_fp_to_sbv

Method test_fp_to_sbv

tests/test_z3_ported.py:3934–3937  ·  view source on GitHub ↗
(self)

Source from the content-addressed store, hash-verified

3932 assert isinstance(result, ArithRef)
3933
3934 def test_fp_to_sbv(self):
3935 x = FP("x", Float32())
3936 result = fpToSBV(RNE(), x, BitVecSort(32))
3937 assert isinstance(result, BitVecRef)
3938
3939 def test_fp_to_ubv(self):
3940 x = FP("x", Float32())

Callers

nothing calls this directly

Calls 5

FPFunction · 0.90
Float32Function · 0.90
fpToSBVFunction · 0.90
RNEFunction · 0.90
BitVecSortFunction · 0.90

Tested by

no test coverage detected