Treat numeric transmute specially

Fixes issues with integer binary operations with floating point numbers transmuted to integers. Fixes facebookexperimental#1252 (comment)
Zeta611 · Nov 17, 2023 · 51eb521 · 51eb521
1 parent a23ff7e
commit 51eb521
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/checker/src/z3_solver.rs b/checker/src/z3_solver.rs
@@ -1139,8 +1139,12 @@ impl Z3Solver {
             Expression::TaggedExpression { operand, .. } => {
                 self.get_as_numeric_z3_ast(&operand.expression)
             }
-            Expression::Transmute { operand, .. } => {
-                self.get_as_numeric_z3_ast(&operand.expression)
+            Expression::Transmute { operand, target_type } => {
+                if target_type.is_integer() || target_type.is_floating_point_number() {
+                    self.numeric_cast(&operand.expression, *target_type)
+                } else {
+                    self.get_as_numeric_z3_ast(&operand.expression)
+                }
             }
             Expression::Top | Expression::Bottom => unsafe {
                 (