Deterministic sqrt test

formalsec · Feb 15, 2024 · a08d285 · a08d285
1 parent 92ae625
commit a08d285
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/test/regression/test_sqrt.smtml b/test/regression/test_sqrt.smtml
@@ -1,5 +1,7 @@
 (set-logic QF_BVFP)
 (let-const x f32)
-(assert (f32.eq (f32.sqrt x) (f32 0.0)))
+(assert (f32.eq x (f32 4.0)))
+(assert (f32.eq (f32.sqrt x) (f32 2.0)))
 (check-sat)
 (get-model)
+; vim: set ft=scheme:
diff --git a/test/regression/test_sqrt.t b/test/regression/test_sqrt.t
@@ -2,4 +2,4 @@ Test QF_FP sqrt:
   $ smtml test_sqrt.smtml
   sat
   (model
-    (x (f32 -0.)))
+    (x (f32 4.)))