tacas fixes

keram88 · keram88 · commit cc860159e3b5 · 2025-04-18T16:59:24.000-06:00
diff --git a/share/smack/lib/math.c b/share/smack/lib/math.c
@@ -492,7 +492,7 @@ int __isinfl(long double x) {
 
 int __isnanl(long double x) {
   int ret = __VERIFIER_nondet_int();
-  __SMACK_code("@ := if $isnan.bvlongdouble.bool(@) then $1 else $0;", ret, x);
+  __SMACK_code("@ := if $isnan.bvfloat128.bool(@) then $1 else $0;", ret, x);
   return ret;
 }
 

Original file line number	Diff line number	Diff line change
`@@ -492,7 +492,7 @@ int __isinfl(long double x) {`
`492`	`492`
`493`	`493`	`int __isnanl(long double x) {`
`494`	`494`	`int ret = __VERIFIER_nondet_int();`
`495`		`- __SMACK_code("@ := if $isnan.bvlongdouble.bool(@) then $1 else $0;", ret, x);`
	`495`	`+ __SMACK_code("@ := if $isnan.bvfloat128.bool(@) then $1 else $0;", ret, x);`
`496`	`496`	`return ret;`
`497`	`497`	`}`
`498`	`498`