Make test_fp.smt2 faster and fix parsing of fp32 literals

The significand should always have sb - 1 bits.

src/parser/smtlib.ml

@@ -164,7 +164,7 @@ module Term = struct
         match (Expr.view s, Expr.view e, Expr.view m) with
         | Val (Str s'), Val (Str e'), Val (Str m') -> (
           match (String.length s', String.length e', String.length m') with
-          | 3, 10, 26 -> Expr.value (Num (F32 (combine_to_int32 s' e' m')))
+          | 3, 10, 25 -> Expr.value (Num (F32 (combine_to_int32 s' e' m')))
           | 3, 13, 54 -> Expr.value (Num (F64 (combine_to_int64 s' e' m')))
           | _ -> Fmt.failwith "%afp size not supported" pp_loc loc )
         | _ ->

test/smt2/test_fp.smt2

@@ -3,10 +3,14 @@
 (declare-fun x () Float64)
 (declare-fun y () Float64)
 (declare-fun r () Float64)
+(declare-fun u () (_ FloatingPoint 8 24))
 (assert (= x (fp #b0 #b01011100111 #b1111110000101111001101101000100010000000100100100111)))
 (assert (= r (fp #b0 #b01101110011 #b0110100010101111111010000110100110010010111011011000)))
-(assert  (not (= (fp.sqrt roundNearestTiesToEven x) r)))
-(assert  (not (= (fp.max x y) r)))
-(assert  (not (= (fp.add roundNearestTiesToEven x y) r)))
+(assert
+  (let ((?x2 (fp #b0 #b10000000 #b00000000000000000000000)))
+  (let ((?x4 (fp #b0 #b10000001 #b00000000000000000000000)))
+  (= (fp.sqrt roundNearestTiesToEven ?x4) ?x2))))
+(assert (not (= (fp.max x y) r)))
+(assert (not (= (fp.add roundNearestTiesToEven x y) r)))
 (check-sat)
-(exit)
+(exit)

test/smt2/test_smt2.t

@@ -52,4 +52,4 @@ Test BitVector parsing:
 
 Test FloatingPoint parsing:
   $ smtml run test_fp.smt2
-  unsat
+  sat