diff --git a/regressions/smt2/6983-1.expected.out b/regressions/smt2/6983-1.expected.out
new file mode 100644
index 00000000..86facdd8
--- /dev/null
+++ b/regressions/smt2/6983-1.expected.out
@@ -0,0 +1,2 @@
+sat
+sat
diff --git a/regressions/smt2/6983-1.smt2 b/regressions/smt2/6983-1.smt2
new file mode 100644
index 00000000..183dec76
--- /dev/null
+++ b/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)
diff --git a/regressions/smt2/6983-2.expected.out b/regressions/smt2/6983-2.expected.out
new file mode 100644
index 00000000..b99e01ea
--- /dev/null
+++ b/regressions/smt2/6983-2.expected.out
@@ -0,0 +1,4 @@
+sat
+sat
+sat
+sat
diff --git a/regressions/smt2/6983-2.smt2 b/regressions/smt2/6983-2.smt2
new file mode 100644
index 00000000..e6eff398
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/regressions/smt2/6983-3.expected.out b/regressions/smt2/6983-3.expected.out
new file mode 100644
index 00000000..86facdd8
--- /dev/null
+++ b/regressions/smt2/6983-3.expected.out
@@ -0,0 +1,2 @@
+sat
+sat
diff --git a/regressions/smt2/6983-3.smt2 b/regressions/smt2/6983-3.smt2
new file mode 100644
index 00000000..aa59f556
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/regressions/smt2/7026-1.expected.out b/regressions/smt2/7026-1.expected.out
new file mode 100644
index 00000000..3f65111b
--- /dev/null
+++ b/regressions/smt2/7026-1.expected.out
@@ -0,0 +1 @@
+unsat
diff --git a/regressions/smt2/7026-1.smt2 b/regressions/smt2/7026-1.smt2
new file mode 100644
index 00000000..3ec69cda
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/regressions/smt2/7026-2.expected.out b/regressions/smt2/7026-2.expected.out
new file mode 100644
index 00000000..6b8a2c3d
--- /dev/null
+++ b/regressions/smt2/7026-2.expected.out
@@ -0,0 +1 @@
+sat
diff --git a/regressions/smt2/7026-2.smt2 b/regressions/smt2/7026-2.smt2
new file mode 100644
index 00000000..b1f79a06
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/regressions/smt2/7026-3.expected.out b/regressions/smt2/7026-3.expected.out
new file mode 100644
index 00000000..6b8a2c3d
--- /dev/null
+++ b/regressions/smt2/7026-3.expected.out
@@ -0,0 +1 @@
+sat
diff --git a/regressions/smt2/7026-3.smt2 b/regressions/smt2/7026-3.smt2
new file mode 100644
index 00000000..03ea5c89
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/regressions/smt2/7026-4.expected.out b/regressions/smt2/7026-4.expected.out
new file mode 100644
index 00000000..6b8a2c3d
--- /dev/null
+++ b/regressions/smt2/7026-4.expected.out
@@ -0,0 +1 @@
+sat
diff --git a/regressions/smt2/7026-4.smt2 b/regressions/smt2/7026-4.smt2
new file mode 100644
index 00000000..03ea5c89
--- /dev/null
+++ b/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)
\ No newline at end of file
diff --git a/regressions/smt2/7026-4.smt2.expected.out b/regressions/smt2/7026-4.smt2.expected.out
new file mode 100644
index 00000000..6b8a2c3d
--- /dev/null
+++ b/regressions/smt2/7026-4.smt2.expected.out
@@ -0,0 +1 @@
+sat