Method test_add

tests/test_z3_semantic.py:838–839 · view source on GitHub ↗

(self, kernel)

Source from the content-addressed store, hash-verified

836	"""Ground floating-point arithmetic proofs."""
837
838	def test_add(self, kernel):
839	assert _try_prove(fpEQ(fpAdd(RNE(), FPVal(1.5), FPVal(2.5)), FPVal(4.0)))
840
841	def test_sub(self, kernel):
842	assert _try_prove(fpEQ(fpSub(RNE(), FPVal(5.0), FPVal(3.0)), FPVal(2.0)))

nothing calls this directly

_try_proveFunction · 0.90

fpEQFunction · 0.90

fpAddFunction · 0.90

RNEFunction · 0.90

FPValFunction · 0.90

no test coverage detected