start implementing fp fused-mul-add pipeline

[ieee754fpu.git] / fp16mul_test.smt2

diff --git a/fp16mul_test.smt2 b/fp16mul_test.smt2
index 1bf11454a1fda76b281571c9795b3972529be04c..7132a28426c578334a53832eff4b6d1583a93830 100644 (file)
--- a/fp16mul_test.smt2
+++ b/fp16mul_test.smt2
@@ -6,7 +6,8 @@
 ; all the effort to add support in yosys and nmigen for smtlib2 reals and
 ; floating-point numbers.
 
-; run with: z3 -smt2 fpmul_test.smt2
+; run with: z3 -smt2 fp16mul_test.smt2
+(set-logic ALL)
 
 ; create some handy type aliases
 (define-sort bv1 () (_ BitVec 1))
@@ -407,4 +408,4 @@
     rounded_up_normal
     round_up_overflows_normal
     do_round_up_normal
-))
\ No newline at end of file
+))