From 68936743925610fffc80512032153c302b29bb58 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 15 Mar 2026 12:08:59 -0700 Subject: [PATCH] fix: correct misleading API comments in fp.go and JavaExample.java (#9003) * Initial plan * fix: correct misleading API comments in fp.go and JavaExample.java Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- examples/java/JavaExample.java | 2 +- src/api/go/fp.go | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 2a02009af..c999a74d8 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2345,7 +2345,7 @@ class JavaExample if (!five.isGround()) throw new TestFailedException(); - // a free variable is not ground + // an uninterpreted constant is also ground (no bound variables) IntExpr x = ctx.mkIntConst("x"); if (!x.isGround()) throw new TestFailedException(); diff --git a/src/api/go/fp.go b/src/api/go/fp.go index 7905ff3bc..4db2d847e 100644 --- a/src/api/go/fp.go +++ b/src/api/go/fp.go @@ -223,7 +223,7 @@ func (c *Context) MkFPNumeralInt64Uint64(sgn bool, exp int64, sig uint64, sort * return newExpr(c, C.Z3_mk_fpa_numeral_int64_uint64(c.ptr, C.bool(sgn), C.int64_t(exp), C.uint64_t(sig), sort.ptr)) } -// MkFPFMA creates a floating-point fused multiply-add: rm * (t1 * t2) + t3. +// MkFPFMA creates a floating-point fused multiply-add: round((t1 * t2) + t3, rm). func (c *Context) MkFPFMA(rm, t1, t2, t3 *Expr) *Expr { return newExpr(c, C.Z3_mk_fpa_fma(c.ptr, rm.ptr, t1.ptr, t2.ptr, t3.ptr)) }