Add more FP regression tests

regressions/smt2/6983-1.expected.out

@@ -0,0 +1,2 @@
+sat
+sat

regressions/smt2/6983-1.smt2

@@ -0,0 +1,13 @@
+(set-option :model_validate true)
+
+(declare-fun s () (Array (_ BitVec 32) (_ BitVec 8)))
+(assert (fp.leq ((_ to_fp 8 24) (concat (select s (_ bv0 32)) (select s (_ bv1 32)) (select s (_ bv0 32)) (select s (_ bv0 32)))) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))))
+(assert (not (fp.geq ((_ to_fp 8 24) (bvxnor (_ bv0 32) (concat (select s (_ bv0 32)) (select s (_ bv1 32)) (select s (_ bv0 32)) (select s (_ bv0 32))))) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))))
+(check-sat)
+
+(reset)
+
+(define-fun s () (Array (_ BitVec 32) (_ BitVec 8)) (store (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #b00000000) #b00000000000000000000000000000000 #b10000000) #b00000000000000000000000000000001 #b01111111))
+(assert (fp.leq ((_ to_fp 8 24) (concat (select s (_ bv0 32)) (select s (_ bv1 32)) (select s (_ bv0 32)) (select s (_ bv0 32)))) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))))
+(assert (not (fp.geq ((_ to_fp 8 24) (bvxnor (_ bv0 32) (concat (select s (_ bv0 32)) (select s (_ bv1 32)) (select s (_ bv0 32)) (select s (_ bv0 32))))) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))))
+(check-sat)

regressions/smt2/6983-2.expected.out

@@ -0,0 +1,4 @@
+sat
+sat
+sat
+sat

regressions/smt2/6983-2.smt2

@@ -0,0 +1,13 @@
+(set-option :model_validate true)
+
+(declare-const a (_ BitVec 1))
+(check-sat)
+(assert (not (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) ((_ to_fp 8 24) (bvnand (_ bv1 32) ((_ zero_extend 31) a))))))
+(check-sat)
+
+(reset)
+
+(define-fun a () (_ BitVec 1) #b0)
+(check-sat)
+(assert (not (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) ((_ to_fp 8 24) (bvnand (_ bv1 32) ((_ zero_extend 31) a))))))
+(check-sat)

regressions/smt2/6983-3.expected.out

@@ -0,0 +1,2 @@
+sat
+sat

regressions/smt2/6983-3.smt2

@@ -0,0 +1,11 @@
+(set-option :model_validate true)
+
+(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
+(assert (bvsgt (_ bv0 64) (bvsmod (concat (select a (_ bv0 32)) (select a (_ bv1 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32))) ((_ sign_extend 32) (ite (fp.lt (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)) ((_ to_fp 11 53) (bvnand (_ bv1 64) (concat (select a (_ bv0 32)) (select a (_ bv1 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)))))) (_ bv1 32) (_ bv0 32))))))
+(check-sat)
+
+(reset)
+
+(define-fun a () (Array (_ BitVec 32) (_ BitVec 8)) (store (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #b00000000) #b00000000000000000000000000000000 #b11111111) #b00000000000000000000000000000001 #b11111111))
+(assert (bvsgt (_ bv0 64) (bvsmod (concat (select a (_ bv0 32)) (select a (_ bv1 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32))) ((_ sign_extend 32) (ite (fp.lt (fp (_ bv0 1) (_ bv0 11) (_ bv0 52)) ((_ to_fp 11 53) (bvnand (_ bv1 64) (concat (select a (_ bv0 32)) (select a (_ bv1 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)) (select a (_ bv0 32)))))) (_ bv1 32) (_ bv0 32))))))
+(check-sat)

regressions/smt2/7026-1.expected.out

@@ -0,0 +1 @@
+unsat

regressions/smt2/7026-1.smt2

@@ -0,0 +1,7 @@
+(set-option :tactic.default_tactic smt)
+(set-option :sat.euf true)
+(set-info :status unsat)
+
+(declare-fun a () Float32)
+(assert (forall ((b Float32)) (not (fp.isPositive (fp.max a b)))))
+(check-sat)

regressions/smt2/7026-2.expected.out

@@ -0,0 +1 @@
+sat

regressions/smt2/7026-2.smt2

@@ -0,0 +1,10 @@
+(set-option :model_validate true)
+(set-option :tactic.default_tactic smt)
+(set-option :sat.euf true)
+(set-info :status sat)
+
+(assert (=
+  ((_ to_fp 5 11) roundTowardNegative (concat (_ bv0 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1)))
+  ((_ to_fp 5 11) roundTowardNegative (concat (_ bv0 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1) (_ bv1 1)))
+  ))
+(check-sat)

regressions/smt2/7026-3.expected.out

@@ -0,0 +1 @@
+sat

regressions/smt2/7026-3.smt2

@@ -0,0 +1,9 @@
+(set-option :model_validate true)
+(set-option :tactic.default_tactic smt)
+(set-option :sat.euf true)
+(set-info :status sat)
+
+(declare-fun p () (_ FloatingPoint 2 3))
+(declare-fun fp () (_ FloatingPoint 2 3))
+(assert (fp.isNegative (fp.fma roundNearestTiesToEven fp p (fp (_ bv0 1) (_ bv0 2) (_ bv0 2)))))
+(check-sat)

regressions/smt2/7026-4.expected.out

@@ -0,0 +1 @@
+sat

regressions/smt2/7026-4.smt2

@@ -0,0 +1,9 @@
+(set-option :model_validate true)
+(set-option :tactic.default_tactic smt)
+(set-option :sat.euf true)
+(set-info :status sat)
+
+(declare-fun p () (_ FloatingPoint 2 3))
+(declare-fun fp () (_ FloatingPoint 2 3))
+(assert (fp.isNegative (fp.fma roundNearestTiesToEven fp p (fp (_ bv0 1) (_ bv0 2) (_ bv0 2)))))
+(check-sat)

regressions/smt2/7026-4.smt2.expected.out

@@ -0,0 +1 @@
+sat