diff --git a/src/parser/smtlib.ml b/src/parser/smtlib.ml index 1411f866..ecef3ec8 100644 --- a/src/parser/smtlib.ml +++ b/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 ) | _ -> diff --git a/test/smt2/test_fp.smt2 b/test/smt2/test_fp.smt2 index 559cde75..6c2d047e 100644 --- a/test/smt2/test_fp.smt2 +++ b/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) \ No newline at end of file +(exit) diff --git a/test/smt2/test_smt2.t b/test/smt2/test_smt2.t index 24bac410..6e9b2990 100644 --- a/test/smt2/test_smt2.t +++ b/test/smt2/test_smt2.t @@ -52,4 +52,4 @@ Test BitVector parsing: Test FloatingPoint parsing: $ smtml run test_fp.smt2 - unsat + sat