packages feed

crackNum 4.6 → 4.7

raw patch · 433 files changed

+7618/−251 lines, 433 filesdep +tasty-hunit

Dependencies added: tasty-hunit

This diff is very large; some files are shown as “too large to diff”. Download the raw patch for the complete diff.

Files

CHANGES.md view
@@ -1,8 +1,21 @@ * Hackage: <http://hackage.haskell.org/package/crackNum> * GitHub:  <http://github.com/LeventErkok/crackNum/> -* Latest Hackage released version: 4.6, 2026-09-03+* Latest Hackage released version: 4.7, 2026-09-04 +### Version 4.7, 2026-09-04++  * Encoding now applies the selected rounding mode directly to the input value.+    Single- and double-precision decimal inputs previously went through Haskell's+    default round-to-nearest conversion first, E4M3 used round-to-nearest in its+    ordinary range, and exact decimal or hexadecimal inputs to the small AI formats+    could be rounded twice. These cases can now produce different, correctly rounded+    bit patterns for `RNA`, `RTP`, `RTN`, and `RTZ`, and near exact midpoints.++  * Corrected directed rounding for E4M3 values between 240 and 448 (and their+    negative counterparts). The implementation previously chose the nearest value+    first and consulted the rounding mode only on exact ties.+ ### Version 4.6, 2026-09-03    * New floating-point format: UE5M3, selected with `-fue5m3`. This is the unsigned@@ -12,23 +25,6 @@     exponent bit is what the format is for: it drops the smallest non-zero value from     `E4M3`'s 2^-9 to the subnormal 2^-17, so a block of small-magnitude elements gets     a scale that can actually represent it.--  * Being a variant of `E4M3`, UE5M3 inherits its deviations from IEEE rather than the-    IEEE reading of the same field widths: there are no infinities, and the all-ones-    pattern is the one and only NaN. Having no sign bit, that is a single pattern-    (`0xFF`) where `E4M3` has one per sign. The rest of the top binade therefore stays-    finite, so the largest representable value is 114688 -- `E4M3`'s 448 carried up the-    eight binades the extra exponent bit buys -- and not the 61440 an IEEE format of-    this shape would stop at. Below that it is ordinary: zero, subnormals, and normals-    all behave as IEEE says, with a bias of 15.--  * Negative inputs are rejected rather than clamped. With no sign bit there is no-    direction to saturate towards, and clamping would quietly turn the value positive;-    this is the same call `E8M0` already makes, and it applies to a negative zero too.-    Values above the range become NaN, following `E4M3`, which likewise has no infinity-    to saturate to.--  * All four GUIs offer the new format, in the "AI formats" group.  ### Version 4.5, 2026-09-01
+ Golds/badInvocation0.gold view
@@ -0,0 +1,6 @@+Arguments: -f3+4 0b01+Exit code: ExitFailure 1++STDERR:+ERROR:+  Input needs to be 7 bits wide, it's too short by 5 bits
+ Golds/badInvocation1.gold view
@@ -0,0 +1,6 @@+Arguments: -f3+4 0xFFFF+Exit code: ExitFailure 1++STDERR:+ERROR:+  Input needs to be 7 bits wide, it's too long by 9 bits
+ Golds/badInvocation2.gold view
@@ -0,0 +1,8 @@+Arguments: -f3+1 0.5+Exit code: ExitFailure 1++STDERR:+ERROR:+  The solver does not support this format:+    3 exponent bits, 1 significand bit+  z3 requires at least 2 of each.
+ Golds/badInvocation3.gold view
@@ -0,0 +1,8 @@+Arguments: -f1+3 0b0000+Exit code: ExitFailure 1++STDERR:+ERROR:+  The solver does not support this format:+    1 exponent bit, 3 significand bits+  z3 requires at least 2 of each.
+ Golds/decode0.gold view
@@ -0,0 +1,13 @@+Arguments: -i4       0b0110+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 6 :: IntN 4+                  3210+   Binary layout: 0110+      Hex layout: 6+            Type: Signed 4-bit 2's complement integer+            Sign: Positive+          Binary: 0b110+           Octal: 0o6+         Decimal: 6+             Hex: 0x6
+ Golds/decode1.gold view
@@ -0,0 +1,12 @@+Arguments: -w4       0xE+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 14 :: WordN 4+                  3210+   Binary layout: 1110+      Hex layout: E+            Type: Unsigned 4-bit word+          Binary: 0b1110+           Octal: 0o16+         Decimal: 14+             Hex: 0xe
+ Golds/decode10.gold view
@@ -0,0 +1,17 @@+Arguments: -ftf32 0b0_10000000_0100000000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 2.5 :: FloatingPoint 8 11+                  1          0+                  8 76543210 9876543210+                  S ---E8--- ---S10----+   Binary layout: 0 10000000 0100000000+      Hex layout: 2 0100+       Precision: 8 exponent bits, 10 significand bits+            Sign: Positive+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1.01p1+           Octal: 0o2.4+         Decimal: 2.5+             Hex: 0x2.8
+ Golds/decode2.gold view
@@ -0,0 +1,14 @@+Arguments: -f3+4     0b0111001+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = NaN :: FloatingPoint 3 4+                  6 543 210+                  S E3- S3-+   Binary layout: 0 111 001+      Hex layout: 39+       Precision: 3 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 4 (Stored: 7, Bias: 3)+  Classification: FP_NAN (Signaling)+           Value: NaN+            Note: Representation for NaN's is not unique
+ Golds/decode3.gold view
@@ -0,0 +1,17 @@+Arguments: -fbp      0x000F+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1.37753e-39 :: FloatingPoint 8 8+                  1      0+                  5 43210987 6543210+                  S ---E8--- --S7---+   Binary layout: 0 00000000 0001111+      Hex layout: 000F+       Precision: 8 exponent bits, 7 significand bits+            Sign: Positive+        Exponent: -126 (Subnormal, with fixed exponent value. Stored: 0, Bias: 127)+  Classification: FP_SUBNORMAL+          Binary: 0b1.111p-130+           Octal: 0o7.4p-132+         Decimal: 1.37753e-39+             Hex: 0x7.8p-132
+ Golds/decode4.gold view
@@ -0,0 +1,17 @@+Arguments: -fdp      0x8000000000000000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -0.0 :: Double+                  6    5          4         3         2         1         0+                  3 21098765432 1098765432109876543210987654321098765432109876543210+                  S ----E11---- ------------------------S52-------------------------+   Binary layout: 1 00000000000 0000000000000000000000000000000000000000000000000000+      Hex layout: 8000 0000 0000 0000+       Precision: Double+            Sign: Negative+        Exponent: -1023 (Stored: 0, Bias: 1023)+  Classification: FP_ZERO+          Binary: -0b0.0+           Octal: -0o0.0+         Decimal: -0.0+             Hex: -0o0
+ Golds/decode5.gold view
@@ -0,0 +1,15 @@+Arguments: -fhp      0x7c01+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = NaN :: FloatingPoint 5 11+                  1       0+                  5 43210 9876543210+                  S -E5-- ---S10----+   Binary layout: 0 11111 0000000001+      Hex layout: 7C01+       Precision: Half (5 exponent bits, 10 significand bits.)+            Sign: Positive+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NAN (Signaling)+           Value: NaN+            Note: Representation for NaN's is not unique
+ Golds/decode6.gold view
@@ -0,0 +1,120 @@+Arguments: -fhp  -l8 128'hffffffffffffffffbdffaaffdc71fc60+Exit code: ExitSuccess+== Lane 7 ============================================================+Satisfiable. Model:+  DECODED = NaN :: FloatingPoint 5 11+                  1       0+                  5 43210 9876543210+                  S -E5-- ---S10----+   Binary layout: 1 11111 1111111111+      Hex layout: FFFF+       Precision: Half (5 exponent bits, 10 significand bits.)+            Sign: Negative+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: Representation for NaN's is not unique+== Lane 6 ============================================================+Satisfiable. Model:+  DECODED = NaN :: FloatingPoint 5 11+                  1       0+                  5 43210 9876543210+                  S -E5-- ---S10----+   Binary layout: 1 11111 1111111111+      Hex layout: FFFF+       Precision: Half (5 exponent bits, 10 significand bits.)+            Sign: Negative+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: Representation for NaN's is not unique+== Lane 5 ============================================================+Satisfiable. Model:+  DECODED = NaN :: FloatingPoint 5 11+                  1       0+                  5 43210 9876543210+                  S -E5-- ---S10----+   Binary layout: 1 11111 1111111111+      Hex layout: FFFF+       Precision: Half (5 exponent bits, 10 significand bits.)+            Sign: Negative+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: Representation for NaN's is not unique+== Lane 4 ============================================================+Satisfiable. Model:+  DECODED = NaN :: FloatingPoint 5 11+                  1       0+                  5 43210 9876543210+                  S -E5-- ---S10----+   Binary layout: 1 11111 1111111111+      Hex layout: FFFF+       Precision: Half (5 exponent bits, 10 significand bits.)+            Sign: Negative+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: Representation for NaN's is not unique+== Lane 3 ============================================================+Satisfiable. Model:+  DECODED = -1.4990234 :: FloatingPoint 5 11+                  1       0+                  5 43210 9876543210+                  S -E5-- ---S10----+   Binary layout: 1 01111 0111111111+      Hex layout: BDFF+       Precision: Half (5 exponent bits, 10 significand bits.)+            Sign: Negative+        Exponent: 0 (Stored: 15, Bias: 15)+  Classification: FP_NORMAL+          Binary: -0b1.0111111111+           Octal: -0o1.3774+         Decimal: -1.4990234+             Hex: -0x1.7fc+== Lane 2 ============================================================+Satisfiable. Model:+  DECODED = -0.054656982 :: FloatingPoint 5 11+                  1       0+                  5 43210 9876543210+                  S -E5-- ---S10----+   Binary layout: 1 01010 1011111111+      Hex layout: AAFF+       Precision: Half (5 exponent bits, 10 significand bits.)+            Sign: Negative+        Exponent: -5 (Stored: 10, Bias: 15)+  Classification: FP_NORMAL+          Binary: -0b1.1011111111p-5+           Octal: -0o3.377p-6+         Decimal: -0.054656982+             Hex: -0xd.fep-8+== Lane 1 ============================================================+Satisfiable. Model:+  DECODED = -284.25 :: FloatingPoint 5 11+                  1       0+                  5 43210 9876543210+                  S -E5-- ---S10----+   Binary layout: 1 10111 0001110001+      Hex layout: DC71+       Precision: Half (5 exponent bits, 10 significand bits.)+            Sign: Negative+        Exponent: 8 (Stored: 23, Bias: 15)+  Classification: FP_NORMAL+          Binary: -0b1.0001110001p8+           Octal: -0o4.342p6+         Decimal: -284.25+             Hex: -0x1.1c4p8+== Lane 0 ============================================================+Satisfiable. Model:+  DECODED = NaN :: FloatingPoint 5 11+                  1       0+                  5 43210 9876543210+                  S -E5-- ---S10----+   Binary layout: 1 11111 0001100000+      Hex layout: FC60+       Precision: Half (5 exponent bits, 10 significand bits.)+            Sign: Negative+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NAN (Signaling)+           Value: NaN+            Note: Representation for NaN's is not unique
+ Golds/decode7.gold view
@@ -0,0 +1,16 @@+Arguments: -fe5m2    0b01111011+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 57300 :: E5M2+                  7 65432 10+                  S -E5-- S2+   Binary layout: 0 11110 11+      Hex layout: 7B+       Precision: 5 exponent bits, 2 significand bits+            Sign: Positive+        Exponent: 15 (Stored: 30, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.11p15+           Octal: 0o1.6p15+         Decimal: 57300+             Hex: 0xep12
+ Golds/decode8.gold view
@@ -0,0 +1,12 @@+Arguments: -w2 -rRNE 2'h1+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1 :: WordN 2+                  10+   Binary layout: 01+      Hex layout: 1+            Type: Unsigned 2-bit word+          Binary: 0b1+           Octal: 0o1+         Decimal: 1+             Hex: 0x1
+ Golds/decode9.gold view
@@ -0,0 +1,17 @@+Arguments: -ftf32 19'h0000F+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1.7219156e-40 :: FloatingPoint 8 11+                  1          0+                  8 76543210 9876543210+                  S ---E8--- ---S10----+   Binary layout: 0 00000000 0000001111+      Hex layout: 0 000F+       Precision: 8 exponent bits, 10 significand bits+            Sign: Positive+        Exponent: -126 (Subnormal, with fixed exponent value. Stored: 0, Bias: 127)+  Classification: FP_SUBNORMAL+          Binary: 0b1.111p-133+           Octal: 0o7.4p-135+         Decimal: 1.7219156e-40+             Hex: 0xfp-136
+ Golds/decodeE4M3_+NaN.gold view
@@ -0,0 +1,14 @@+Arguments: -fe4m3 0b_0111_1111+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = NaN :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 111+      Hex layout: 7F+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: Representation for NaN's is not unique
+ Golds/decodeE4M3_-256.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b11111000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -256.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 000+      Hex layout: F8+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1p+8+           Octal: -0o4p+6+         Decimal: -256.0+             Hex: -0x1p+8
+ Golds/decodeE4M3_-288.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b11111001+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -288.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 001+      Hex layout: F9+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.001p+8+           Octal: -0o4.4p+6+         Decimal: -288.0+             Hex: -0x1.2p+8
+ Golds/decodeE4M3_-320.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b11111010+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -320.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 010+      Hex layout: FA+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.01p+8+           Octal: -0o5p+6+         Decimal: -320.0+             Hex: -0x1.4p+8
+ Golds/decodeE4M3_-352.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b11111011+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -352.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 011+      Hex layout: FB+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.011p+8+           Octal: -0o5.4p+6+         Decimal: -352.0+             Hex: -0x1.6p+8
+ Golds/decodeE4M3_-384.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b11111100+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -384.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 100+      Hex layout: FC+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.1p+8+           Octal: -0o6p+6+         Decimal: -384.0+             Hex: -0x1.8p+8
+ Golds/decodeE4M3_-416.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b11111101+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 101+      Hex layout: FD+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.101p+8+           Octal: -0o6.4p+6+         Decimal: -416.0+             Hex: -0x1.ap+8
+ Golds/decodeE4M3_-448.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b11111110+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -448.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 110+      Hex layout: FE+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.11p+8+           Octal: -0o7p+6+         Decimal: -448.0+             Hex: -0x1.cp+8
+ Golds/decodeE4M3_-NaN.gold view
@@ -0,0 +1,14 @@+Arguments: -fe4m3 0b_1111_1111+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = NaN :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 111+      Hex layout: FF+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: Representation for NaN's is not unique
+ Golds/decodeE4M3_256.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b01111000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 256.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 000+      Hex layout: 78+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1p+8+           Octal: 0o4p+6+         Decimal: 256.0+             Hex: 0x1p+8
+ Golds/decodeE4M3_288.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b01111001+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 288.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 001+      Hex layout: 79+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.001p+8+           Octal: 0o4.4p+6+         Decimal: 288.0+             Hex: 0x1.2p+8
+ Golds/decodeE4M3_320.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b01111010+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 320.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 010+      Hex layout: 7A+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.01p+8+           Octal: 0o5p+6+         Decimal: 320.0+             Hex: 0x1.4p+8
+ Golds/decodeE4M3_352.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b01111011+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 352.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 011+      Hex layout: 7B+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.011p+8+           Octal: 0o5.4p+6+         Decimal: 352.0+             Hex: 0x1.6p+8
+ Golds/decodeE4M3_384.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b01111100+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 384.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 100+      Hex layout: 7C+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.1p+8+           Octal: 0o6p+6+         Decimal: 384.0+             Hex: 0x1.8p+8
+ Golds/decodeE4M3_416.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b01111101+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 101+      Hex layout: 7D+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.101p+8+           Octal: 0o6.4p+6+         Decimal: 416.0+             Hex: 0x1.ap+8
+ Golds/decodeE4M3_448.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b01111110+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 448.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 110+      Hex layout: 7E+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.11p+8+           Octal: 0o7p+6+         Decimal: 448.0+             Hex: 0x1.cp+8
+ Golds/decodeE4M3_regular_00000000.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b00000000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 0.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 0000 000+      Hex layout: 00+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: -7 (Stored: 0, Bias: 7)+  Classification: FP_ZERO+          Binary: 0b0.0+           Octal: 0o0.0+         Decimal: 0.0+             Hex: 0x0
+ Golds/decodeE4M3_regular_00000001.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b00000001+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 0.001953 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 0000 001+      Hex layout: 01+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: -6 (Subnormal, with fixed exponent value. Stored: 0, Bias: 7)+  Classification: FP_SUBNORMAL+          Binary: 0b1p-9+           Octal: 0o1p-9+         Decimal: 0.001953+             Hex: 0x8p-12
+ Golds/decodeE4M3_regular_00111000.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b00111000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 0111 000+      Hex layout: 38+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 0 (Stored: 7, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1
+ Golds/decodeE4M3_regular_01110111.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b01110111+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1110 111+      Hex layout: 77+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.111p7+           Octal: 0o3.6p6+         Decimal: 240.0+             Hex: 0xfp4
+ Golds/decodeE4M3_regular_10000000.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b10000000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -0.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 0000 000+      Hex layout: 80+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: -7 (Stored: 0, Bias: 7)+  Classification: FP_ZERO+          Binary: -0b0.0+           Octal: -0o0.0+         Decimal: -0.0+             Hex: -0o0
+ Golds/decodeE4M3_regular_10111100.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 0b10111100+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -1.5 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 0111 100+      Hex layout: BC+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 0 (Stored: 7, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.1+           Octal: -0o1.4+         Decimal: -1.5+             Hex: -0x1.8
+ Golds/decodeE8M0_00.gold view
@@ -0,0 +1,16 @@+Arguments: -fe8m0 0x00+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 5.877471754111438e-39 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 00000000+      Hex layout: 00+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: -127 (Stored: 0, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p-127+           Octal: 0o4p-129+         Decimal: 5.877471754111438e-39+             Hex: 0x2p-128
+ Golds/decodeE8M0_01.gold view
@@ -0,0 +1,16 @@+Arguments: -fe8m0 0x01+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1.1754943508222875e-38 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 00000001+      Hex layout: 01+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: -126 (Stored: 1, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p-126+           Octal: 0o1p-126+         Decimal: 1.1754943508222875e-38+             Hex: 0x4p-128
+ Golds/decodeE8M0_7F.gold view
@@ -0,0 +1,16 @@+Arguments: -fe8m0 0x7F+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 01111111+      Hex layout: 7F+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 0 (Stored: 127, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1
+ Golds/decodeE8M0_80.gold view
@@ -0,0 +1,16 @@+Arguments: -fe8m0 0x80+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 2.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000000+      Hex layout: 80+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2
+ Golds/decodeE8M0_FD.gold view
@@ -0,0 +1,16 @@+Arguments: -fe8m0 0xFD+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 8.507059173023462e37 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 11111101+      Hex layout: FD+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 126 (Stored: 253, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+126+           Octal: 0o1p+126+         Decimal: 8.507059173023462e37+             Hex: 0x4p+124
+ Golds/decodeE8M0_FE.gold view
@@ -0,0 +1,16 @@+Arguments: -fe8m0 0xFE+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1.7014118346046923e38 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 11111110+      Hex layout: FE+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 127 (Stored: 254, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+127+           Octal: 0o2p+126+         Decimal: 1.7014118346046923e38+             Hex: 0x8p+124
+ Golds/decodeE8M0_FF.gold view
@@ -0,0 +1,13 @@+Arguments: -fe8m0 0xFF+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = NaN :: E8M0+                  76543210+                  ---E8---+   Binary layout: 11111111+      Hex layout: FF+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_NAN+           Value: NaN
+ Golds/decodeFP4E0M3_0000.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b0000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 000+      Hex layout: 0+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b0+           Octal: 0o0+         Decimal: 0+             Hex: 0x0
+ Golds/decodeFP4E0M3_0001.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b0001+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 001+      Hex layout: 1+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b1+           Octal: 0o1+         Decimal: 1+             Hex: 0x1
+ Golds/decodeFP4E0M3_0010.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b0010+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 010+      Hex layout: 2+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b10+           Octal: 0o2+         Decimal: 2+             Hex: 0x2
+ Golds/decodeFP4E0M3_0011.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b0011+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 011+      Hex layout: 3+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b11+           Octal: 0o3+         Decimal: 3+             Hex: 0x3
+ Golds/decodeFP4E0M3_0100.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b0100+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 100+      Hex layout: 4+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b100+           Octal: 0o4+         Decimal: 4+             Hex: 0x4
+ Golds/decodeFP4E0M3_0101.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b0101+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 101+      Hex layout: 5+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b101+           Octal: 0o5+         Decimal: 5+             Hex: 0x5
+ Golds/decodeFP4E0M3_0110.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b0110+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 110+      Hex layout: 6+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b110+           Octal: 0o6+         Decimal: 6+             Hex: 0x6
+ Golds/decodeFP4E0M3_0111.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b0111+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 111+      Hex layout: 7+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b111+           Octal: 0o7+         Decimal: 7+             Hex: 0x7
+ Golds/decodeFP4E0M3_1000.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b1000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 000+      Hex layout: 8+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b0+           Octal: -0o0+         Decimal: -0+             Hex: -0x0
+ Golds/decodeFP4E0M3_1001.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b1001+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -1 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 001+      Hex layout: 9+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b1+           Octal: -0o1+         Decimal: -1+             Hex: -0x1
+ Golds/decodeFP4E0M3_1010.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b1010+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 010+      Hex layout: A+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b10+           Octal: -0o2+         Decimal: -2+             Hex: -0x2
+ Golds/decodeFP4E0M3_1011.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b1011+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 011+      Hex layout: B+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b11+           Octal: -0o3+         Decimal: -3+             Hex: -0x3
+ Golds/decodeFP4E0M3_1100.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b1100+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 100+      Hex layout: C+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b100+           Octal: -0o4+         Decimal: -4+             Hex: -0x4
+ Golds/decodeFP4E0M3_1101.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b1101+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 101+      Hex layout: D+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b101+           Octal: -0o5+         Decimal: -5+             Hex: -0x5
+ Golds/decodeFP4E0M3_1110.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b1110+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 110+      Hex layout: E+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b110+           Octal: -0o6+         Decimal: -6+             Hex: -0x6
+ Golds/decodeFP4E0M3_1111.gold view
@@ -0,0 +1,14 @@+Arguments: -ffp4e0m3 0b1111+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 111+      Hex layout: F+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b111+           Octal: -0o7+         Decimal: -7+             Hex: -0x7
+ Golds/decodeFP4_0000.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b0000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 0.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 0+      Hex layout: 0+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: -1 (Stored: 0, Bias: 1)+  Classification: FP_ZERO+          Binary: 0b0.0+           Octal: 0o0.0+         Decimal: 0.0+             Hex: 0x0
+ Golds/decodeFP4_0001.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b0001+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 1+      Hex layout: 1+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: 0b1p-1+           Octal: 0o4p-3+         Decimal: 0.5+             Hex: 0x8p-4
+ Golds/decodeFP4_0010.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b0010+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 0+      Hex layout: 2+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1
+ Golds/decodeFP4_0011.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b0011+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 1+      Hex layout: 3+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1+           Octal: 0o1.4+         Decimal: 1.5+             Hex: 0x1.8
+ Golds/decodeFP4_0100.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b0100+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 0+      Hex layout: 4+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2
+ Golds/decodeFP4_0101.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b0101+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 3.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 1+      Hex layout: 5+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p1+           Octal: 0o3+         Decimal: 3.0+             Hex: 0x3
+ Golds/decodeFP4_0110.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b0110+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 0+      Hex layout: 6+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4
+ Golds/decodeFP4_0111.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b0111+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6
+ Golds/decodeFP4_1000.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b1000+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -0.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 00 0+      Hex layout: 8+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: -1 (Stored: 0, Bias: 1)+  Classification: FP_ZERO+          Binary: -0b0.0+           Octal: -0o0.0+         Decimal: -0.0+             Hex: -0o0
+ Golds/decodeFP4_1001.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b1001+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 00 1+      Hex layout: 9+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: -0b1p-1+           Octal: -0o4p-3+         Decimal: -0.5+             Hex: -0x8p-4
+ Golds/decodeFP4_1010.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b1010+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 0+      Hex layout: A+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1+           Octal: -0o1+         Decimal: -1.0+             Hex: -0x1
+ Golds/decodeFP4_1011.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b1011+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 1+      Hex layout: B+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1+           Octal: -0o1.4+         Decimal: -1.5+             Hex: -0x1.8
+ Golds/decodeFP4_1100.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b1100+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 0+      Hex layout: C+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p1+           Octal: -0o2+         Decimal: -2.0+             Hex: -0x2
+ Golds/decodeFP4_1101.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b1101+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -3.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 1+      Hex layout: D+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p1+           Octal: -0o3+         Decimal: -3.0+             Hex: -0x3
+ Golds/decodeFP4_1110.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b1110+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 0+      Hex layout: E+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p+2+           Octal: -0o4+         Decimal: -4.0+             Hex: -0x4
+ Golds/decodeFP4_1111.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4 0b1111+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = -6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 1+      Hex layout: F+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p+2+           Octal: -0o6+         Decimal: -6.0+             Hex: -0x6
+ Golds/decodeUE5M3_00.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3 0x00+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 0.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 00000 000+      Hex layout: 00+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: -15 (Stored: 0, Bias: 15)+  Classification: FP_ZERO+          Binary: 0b0.0+           Octal: 0o0.0+         Decimal: 0.0+             Hex: 0x0
+ Golds/decodeUE5M3_01.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3 0x01+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 0.000007629 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 00000 001+      Hex layout: 01+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: -14 (Subnormal, with fixed exponent value. Stored: 0, Bias: 15)+  Classification: FP_SUBNORMAL+          Binary: 0b1p-17+           Octal: 0o2p-18+         Decimal: 0.000007629+             Hex: 0x8p-20
+ Golds/decodeUE5M3_07.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3 0x07+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 0.00005341 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 00000 111+      Hex layout: 07+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: -14 (Subnormal, with fixed exponent value. Stored: 0, Bias: 15)+  Classification: FP_SUBNORMAL+          Binary: 0b1.11p-15+           Octal: 0o1.6p-15+         Decimal: 0.00005341+             Hex: 0x3.8p-16
+ Golds/decodeUE5M3_08.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3 0x08+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 0.00006104 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 00001 000+      Hex layout: 08+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: -14 (Stored: 1, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1p-14+           Octal: 0o2p-15+         Decimal: 0.00006104+             Hex: 0x4p-16
+ Golds/decodeUE5M3_78.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3 0x78+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 1.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 01111 000+      Hex layout: 78+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 0 (Stored: 15, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1
+ Golds/decodeUE5M3_F7.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3 0xF7+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 61440 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11110 111+      Hex layout: F7+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 15 (Stored: 30, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.111p15+           Octal: 0o1.7p15+         Decimal: 61440+             Hex: 0xfp12
+ Golds/decodeUE5M3_F8.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3 0xF8+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 65536.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 000+      Hex layout: F8+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1p+16+           Octal: 0o2p+15+         Decimal: 65536.0+             Hex: 0x1p+16
+ Golds/decodeUE5M3_FB.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3 0xFB+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 90112.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 011+      Hex layout: FB+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.011p+16+           Octal: 0o2.6p+15+         Decimal: 90112.0+             Hex: 0x1.6p+16
+ Golds/decodeUE5M3_FE.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3 0xFE+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = 114688.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 110+      Hex layout: FE+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.11p+16+           Octal: 0o3.4p+15+         Decimal: 114688.0+             Hex: 0x1.cp+16
+ Golds/decodeUE5M3_FF.gold view
@@ -0,0 +1,13 @@+Arguments: -fue5m3 0xFF+Exit code: ExitSuccess+Satisfiable. Model:+  DECODED = NaN :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 111+      Hex layout: FF+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NAN+           Value: NaN
+ Golds/encode0.gold view
@@ -0,0 +1,13 @@+Arguments: -i4 -- -2+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2 :: IntN 4+                  3210+   Binary layout: 1110+      Hex layout: E+            Type: Signed 4-bit 2's complement integer+            Sign: Negative+          Binary: -0b10+           Octal: -0o2+         Decimal: -2+             Hex: -0x2
+ Golds/encode1.gold view
@@ -0,0 +1,12 @@+Arguments: -w4 2+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2 :: WordN 4+                  3210+   Binary layout: 0010+      Hex layout: 2+            Type: Unsigned 4-bit word+          Binary: 0b10+           Octal: 0o2+         Decimal: 2+             Hex: 0x2
+ Golds/encode10.gold view
@@ -0,0 +1,16 @@+Arguments: -f3+3     nan+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: FloatingPoint 3 3+                  5 432 10+                  S E3- S2+   Binary layout: 0 111 10+      Hex layout: 1E+       Precision: 3 exponent bits, 2 significand bits+            Sign: Positive+        Exponent: 4 (Stored: 7, Bias: 3)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: Representation for NaN's is not unique+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "nan" was exact. No rounding happened.
+ Golds/encode11.gold view
@@ -0,0 +1,16 @@+Arguments: -fsp  -- -inf+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -Infinity :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------+   Binary layout: 1 11111111 00000000000000000000000+      Hex layout: FF80 0000+       Precision: Single+            Sign: Negative+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_INFINITE+           Value: -Infinity+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "-inf" was exact. No rounding happened.
+ Golds/encode12.gold view
@@ -0,0 +1,16 @@+Arguments: -fsp  -- -infinity+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -Infinity :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------+   Binary layout: 1 11111111 00000000000000000000000+      Hex layout: FF80 0000+       Precision: Single+            Sign: Negative+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_INFINITE+           Value: -Infinity+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "-infinity" was exact. No rounding happened.
+ Golds/encode13.gold view
@@ -0,0 +1,16 @@+Arguments: -fsp      inf+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = Infinity :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------+   Binary layout: 0 11111111 00000000000000000000000+      Hex layout: 7F80 0000+       Precision: Single+            Sign: Positive+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_INFINITE+           Value: Infinity+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "inf" was exact. No rounding happened.
+ Golds/encode14.gold view
@@ -0,0 +1,16 @@+Arguments: -fsp      infinity+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = Infinity :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------+   Binary layout: 0 11111111 00000000000000000000000+      Hex layout: 7F80 0000+       Precision: Single+            Sign: Positive+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_INFINITE+           Value: Infinity+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "infinity" was exact. No rounding happened.
+ Golds/encode15.gold view
@@ -0,0 +1,17 @@+Arguments: -fsp      nan+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------+   Binary layout: 0 11111111 10000000000000000000000+      Hex layout: 7FC0 0000+       Precision: Single+            Sign: Positive+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: Representation for NaN's is not unique+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "nan" was exact. No rounding happened.
+ Golds/encode16.gold view
@@ -0,0 +1,18 @@+Arguments: -fe5m2 2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.5 :: E5M2+                  7 65432 10+                  S -E5-- S2+   Binary layout: 0 10000 01+      Hex layout: 41+       Precision: 5 exponent bits, 2 significand bits+            Sign: Positive+        Exponent: 1 (Stored: 16, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.01p1+           Octal: 0o2.4+         Decimal: 2.5+             Hex: 0x2.8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "2.5" was exact. No rounding happened.
+ Golds/encode17.gold view
@@ -0,0 +1,17 @@+Arguments: -fsp -- -0x2p3+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -16.0 :: FloatingPoint 8 24+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------+   Binary layout: 1 10000011 00000000000000000000000+      Hex layout: C180 0000+       Precision: Single (8 exponent bits, 23 significand bits.)+            Sign: Negative+        Exponent: 4 (Stored: 131, Bias: 127)+  Classification: FP_NORMAL+          Binary: -0b1p4+           Octal: -0o2p3+         Decimal: -16.0+             Hex: -0x1p4
+ Golds/encode18.gold view
@@ -0,0 +1,17 @@+Arguments: -fdp -- 0x1.3+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.1875 :: FloatingPoint 11 53+                  6     5          4         3         2         1         0+                  4 32109876543 21098765432109876543210987654321098765432109876543210+                  S ----E11---- -------------------------S53-------------------------+   Binary layout: 0 01111111111 00110000000000000000000000000000000000000000000000000+      Hex layout: 0 7FE6 0000 0000 0000+       Precision: 11 exponent bits, 53 significand bits+            Sign: Positive+        Exponent: 0 (Stored: 1023, Bias: 1023)+  Classification: FP_NORMAL+          Binary: 0b1.0011+           Octal: 0o1.14+         Decimal: 1.1875+             Hex: 0x1.3
+ Golds/encode19.gold view
@@ -0,0 +1,17 @@+Arguments: -fhp -- 0x1.3p4+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 19.0 :: FloatingPoint 5 11+                  1       0+                  5 43210 9876543210+                  S -E5-- ---S10----+   Binary layout: 0 10011 0011000000+      Hex layout: 4CC0+       Precision: Half (5 exponent bits, 10 significand bits.)+            Sign: Positive+        Exponent: 4 (Stored: 19, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.0011p4+           Octal: 0o2.3p3+         Decimal: 19.0+             Hex: 0x1.3p4
+ Golds/encode2.gold view
@@ -0,0 +1,18 @@+Arguments: -f3+4 2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.5 :: FloatingPoint 3 4+                  6 543 210+                  S E3- S3-+   Binary layout: 0 100 010+      Hex layout: 22+       Precision: 3 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 1 (Stored: 4, Bias: 3)+  Classification: FP_NORMAL+          Binary: 0b1.01p1+           Octal: 0o2.4+         Decimal: 2.5+             Hex: 0x2.8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "2.5" was exact. No rounding happened.
+ Golds/encode20.gold view
@@ -0,0 +1,19 @@+Arguments: -ftf32 2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.5 :: FloatingPoint 8 11+                  1          0+                  8 76543210 9876543210+                  S ---E8--- ---S10----+   Binary layout: 0 10000000 0100000000+      Hex layout: 2 0100+       Precision: 8 exponent bits, 10 significand bits+            Sign: Positive+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1.01p1+           Octal: 0o2.4+         Decimal: 2.5+             Hex: 0x2.8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "2.5" was exact. No rounding happened.
+ Golds/encode21.gold view
@@ -0,0 +1,16 @@+Arguments: -ftf32 -- -inf+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -Infinity :: FloatingPoint 8 11+                  1          0+                  8 76543210 9876543210+                  S ---E8--- ---S10----+   Binary layout: 1 11111111 0000000000+      Hex layout: 7 FC00+       Precision: 8 exponent bits, 10 significand bits+            Sign: Negative+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_INFINITE+           Value: -Infinity+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "-inf" was exact. No rounding happened.
+ Golds/encode22.gold view
@@ -0,0 +1,17 @@+Arguments: -ftf32    nan+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: FloatingPoint 8 11+                  1          0+                  8 76543210 9876543210+                  S ---E8--- ---S10----+   Binary layout: 0 11111111 1000000000+      Hex layout: 3 FE00+       Precision: 8 exponent bits, 10 significand bits+            Sign: Positive+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: Representation for NaN's is not unique+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "nan" was exact. No rounding happened.
+ Golds/encode3.gold view
@@ -0,0 +1,18 @@+Arguments: -f3+4 2.5 -rRTZ+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.5 :: FloatingPoint 3 4+                  6 543 210+                  S E3- S3-+   Binary layout: 0 100 010+      Hex layout: 22+       Precision: 3 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 1 (Stored: 4, Bias: 3)+  Classification: FP_NORMAL+          Binary: 0b1.01p1+           Octal: 0o2.4+         Decimal: 2.5+             Hex: 0x2.8+   Rounding mode: RTZ: Round towards zero.+            Note: Conversion from "2.5" was exact. No rounding happened.
+ Golds/encode4.gold view
@@ -0,0 +1,19 @@+Arguments: -fbp 2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.5 :: FloatingPoint 8 8+                  1      0+                  5 43210987 6543210+                  S ---E8--- --S7---+   Binary layout: 0 10000000 0100000+      Hex layout: 4020+       Precision: 8 exponent bits, 7 significand bits+            Sign: Positive+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1.01p1+           Octal: 0o2.4+         Decimal: 2.5+             Hex: 0x2.8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "2.5" was exact. No rounding happened.
+ Golds/encode5.gold view
@@ -0,0 +1,19 @@+Arguments: -fdp 2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.5 :: Double+                  6    5          4         3         2         1         0+                  3 21098765432 1098765432109876543210987654321098765432109876543210+                  S ----E11---- ------------------------S52-------------------------+   Binary layout: 0 10000000000 0100000000000000000000000000000000000000000000000000+      Hex layout: 4004 0000 0000 0000+       Precision: Double+            Sign: Positive+        Exponent: 1 (Stored: 1024, Bias: 1023)+  Classification: FP_NORMAL+          Binary: 0b1.01p+1+           Octal: 0o2.4+         Decimal: 2.5+             Hex: 0x2.8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "2.5" was exact. No rounding happened.
+ Golds/encode6.gold view
@@ -0,0 +1,15 @@+Arguments: -f3+3 -- -inf+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -Infinity :: FloatingPoint 3 3+                  5 432 10+                  S E3- S2+   Binary layout: 1 111 00+      Hex layout: 3C+       Precision: 3 exponent bits, 2 significand bits+            Sign: Negative+        Exponent: 4 (Stored: 7, Bias: 3)+  Classification: FP_INFINITE+           Value: -Infinity+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "-inf" was exact. No rounding happened.
+ Golds/encode7.gold view
@@ -0,0 +1,15 @@+Arguments: -f3+3 -- -infinity+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -Infinity :: FloatingPoint 3 3+                  5 432 10+                  S E3- S2+   Binary layout: 1 111 00+      Hex layout: 3C+       Precision: 3 exponent bits, 2 significand bits+            Sign: Negative+        Exponent: 4 (Stored: 7, Bias: 3)+  Classification: FP_INFINITE+           Value: -Infinity+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "-infinity" was exact. No rounding happened.
+ Golds/encode8.gold view
@@ -0,0 +1,15 @@+Arguments: -f3+3     inf+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = Infinity :: FloatingPoint 3 3+                  5 432 10+                  S E3- S2+   Binary layout: 0 111 00+      Hex layout: 1C+       Precision: 3 exponent bits, 2 significand bits+            Sign: Positive+        Exponent: 4 (Stored: 7, Bias: 3)+  Classification: FP_INFINITE+           Value: Infinity+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "inf" was exact. No rounding happened.
+ Golds/encode9.gold view
@@ -0,0 +1,15 @@+Arguments: -f3+3     infinity+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = Infinity :: FloatingPoint 3 3+                  5 432 10+                  S E3- S2+   Binary layout: 0 111 00+      Hex layout: 1C+       Precision: 3 exponent bits, 2 significand bits+            Sign: Positive+        Exponent: 4 (Stored: 7, Bias: 3)+  Classification: FP_INFINITE+           Value: Infinity+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "infinity" was exact. No rounding happened.
+ Golds/encodeE4M3_+inf.gold view
@@ -0,0 +1,14 @@+Arguments: -fe4m3    inf+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 111+      Hex layout: 7F+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: The input value was infinite, which is not representable in E4M3.
+ Golds/encodeE4M3_-inf.gold view
@@ -0,0 +1,14 @@+Arguments: -fe4m3 -- -inf+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 111+      Hex layout: 7F+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: The input value was infinite, which is not representable in E4M3.
+ Golds/encodeE4M3_bnd1.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 -- -239.9999+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1110 111+      Hex layout: F7+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.111p7+           Octal: -0o3.6p6+         Decimal: -240.0+             Hex: -0xfp4
+ Golds/encodeE4M3_bnd2.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 --  239.9999+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1110 111+      Hex layout: 77+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.111p7+           Octal: 0o3.6p6+         Decimal: 240.0+             Hex: 0xfp4
+ Golds/encodeE4M3_in1.gold view
@@ -0,0 +1,15 @@+Arguments: -fe4m3 -- -448.0001+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 111+      Hex layout: 7F+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: The input value -448.0001 is out of bounds, and hence becomes NaN+                  The representable range is [-448, 448]
+ Golds/encodeE4M3_in2.gold view
@@ -0,0 +1,15 @@+Arguments: -fe4m3 --  448.0001+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 111+      Hex layout: 7F+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NAN (Quiet)+           Value: NaN+            Note: The input value 448.0001 is out of bounds, and hence becomes NaN+                  The representable range is [-448, 448]
+ Golds/encodeE4M3_mr1.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 --   240+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1110 111+      Hex layout: 77+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.111p7+           Octal: 0o3.6p6+         Decimal: 240.0+             Hex: 0xfp4
+ Golds/encodeE4M3_mr2.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 --   240.00+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1110 111+      Hex layout: 77+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.111p7+           Octal: 0o3.6p6+         Decimal: 240.0+             Hex: 0xfp4
+ Golds/encodeE4M3_mr3.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 --  -240+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1110 111+      Hex layout: F7+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.111p7+           Octal: -0o3.6p6+         Decimal: -240.0+             Hex: -0xfp4
+ Golds/encodeE4M3_mr4.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 --  -240.00+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1110 111+      Hex layout: F7+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.111p7+           Octal: -0o3.6p6+         Decimal: -240.0+             Hex: -0xfp4
+ Golds/encodeE4M3_nan.gold view
@@ -0,0 +1,13 @@+Arguments: -fe4m3    nan+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 111+      Hex layout: 7F+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NAN (Quiet)+           Value: NaN
+ Golds/encodeE4M3_special_RNA_+240.01.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNA --  240.01+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1110 111+      Hex layout: 77+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.111p+7+           Octal: 0o3.6p+6+         Decimal: 240.0+             Hex: 0xFp+4+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 240.01, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNA_+248.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNA --  248.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 256.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 000+      Hex layout: 78+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1p+8+           Octal: 0o4p+6+         Decimal: 256.0+             Hex: 0x1p+8+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 248.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNA_+419.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNA --  419.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 101+      Hex layout: 7d+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.101p+8+           Octal: 0o6.4p+6+         Decimal: 416.0+             Hex: 0x1.Ap+8+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 419.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNA_+432.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNA --  432.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 448.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 110+      Hex layout: 7e+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.11p+8+           Octal: 0o7p+6+         Decimal: 448.0+             Hex: 0x1.Cp+8+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 432.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNA_-240.01.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNA -- -240.01+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1110 111+      Hex layout: f7+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.111p+7+           Octal: -0o3.6p+6+         Decimal: -240.0+             Hex: -0xFp+4+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -240.01, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNA_-248.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNA -- -248.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -256.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 000+      Hex layout: f8+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1p+8+           Octal: -0o4p+6+         Decimal: -256.0+             Hex: -0x1p+8+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -248.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNA_-419.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNA -- -419.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 101+      Hex layout: fd+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.101p+8+           Octal: -0o6.4p+6+         Decimal: -416.0+             Hex: -0x1.Ap+8+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -419.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNA_-432.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNA -- -432.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -448.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 110+      Hex layout: fe+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.11p+8+           Octal: -0o7p+6+         Decimal: -448.0+             Hex: -0x1.Cp+8+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -432.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNE_+240.01.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNE --  240.01+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1110 111+      Hex layout: 77+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.111p+7+           Octal: 0o3.6p+6+         Decimal: 240.0+             Hex: 0xFp+4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 240.01, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNE_+248.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNE --  248.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 256.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 000+      Hex layout: 78+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1p+8+           Octal: 0o4p+6+         Decimal: 256.0+             Hex: 0x1p+8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 248.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNE_+419.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNE --  419.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 101+      Hex layout: 7d+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.101p+8+           Octal: 0o6.4p+6+         Decimal: 416.0+             Hex: 0x1.Ap+8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 419.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNE_+432.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNE --  432.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 448.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 110+      Hex layout: 7e+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.11p+8+           Octal: 0o7p+6+         Decimal: 448.0+             Hex: 0x1.Cp+8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 432.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNE_-240.01.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNE -- -240.01+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1110 111+      Hex layout: f7+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.111p+7+           Octal: -0o3.6p+6+         Decimal: -240.0+             Hex: -0xFp+4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -240.01, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNE_-248.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNE -- -248.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -256.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 000+      Hex layout: f8+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1p+8+           Octal: -0o4p+6+         Decimal: -256.0+             Hex: -0x1p+8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -248.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNE_-419.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNE -- -419.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 101+      Hex layout: fd+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.101p+8+           Octal: -0o6.4p+6+         Decimal: -416.0+             Hex: -0x1.Ap+8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -419.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RNE_-432.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRNE -- -432.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -448.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 110+      Hex layout: fe+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.11p+8+           Octal: -0o7p+6+         Decimal: -448.0+             Hex: -0x1.Cp+8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -432.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTN_+240.01.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTN --  240.01+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1110 111+      Hex layout: 77+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.111p+7+           Octal: 0o3.6p+6+         Decimal: 240.0+             Hex: 0xFp+4+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 240.01, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTN_+248.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTN --  248.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1110 111+      Hex layout: 77+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.111p+7+           Octal: 0o3.6p+6+         Decimal: 240.0+             Hex: 0xFp+4+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 248.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTN_+419.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTN --  419.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 101+      Hex layout: 7d+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.101p+8+           Octal: 0o6.4p+6+         Decimal: 416.0+             Hex: 0x1.Ap+8+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 419.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTN_+432.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTN --  432.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 101+      Hex layout: 7d+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.101p+8+           Octal: 0o6.4p+6+         Decimal: 416.0+             Hex: 0x1.Ap+8+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 432.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTN_-240.01.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTN -- -240.01+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -256.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 000+      Hex layout: f8+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1p+8+           Octal: -0o4p+6+         Decimal: -256.0+             Hex: -0x1p+8+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -240.01, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTN_-248.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTN -- -248.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -256.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 000+      Hex layout: f8+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1p+8+           Octal: -0o4p+6+         Decimal: -256.0+             Hex: -0x1p+8+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -248.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTN_-419.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTN -- -419.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -448.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 110+      Hex layout: fe+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.11p+8+           Octal: -0o7p+6+         Decimal: -448.0+             Hex: -0x1.Cp+8+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -419.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTN_-432.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTN -- -432.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -448.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 110+      Hex layout: fe+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.11p+8+           Octal: -0o7p+6+         Decimal: -448.0+             Hex: -0x1.Cp+8+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -432.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTP_+240.01.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTP --  240.01+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 256.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 000+      Hex layout: 78+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1p+8+           Octal: 0o4p+6+         Decimal: 256.0+             Hex: 0x1p+8+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 240.01, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTP_+248.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTP --  248.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 256.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 000+      Hex layout: 78+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1p+8+           Octal: 0o4p+6+         Decimal: 256.0+             Hex: 0x1p+8+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 248.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTP_+419.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTP --  419.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 448.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 110+      Hex layout: 7e+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.11p+8+           Octal: 0o7p+6+         Decimal: 448.0+             Hex: 0x1.Cp+8+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 419.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTP_+432.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTP --  432.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 448.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 110+      Hex layout: 7e+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.11p+8+           Octal: 0o7p+6+         Decimal: 448.0+             Hex: 0x1.Cp+8+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 432.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTP_-240.01.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTP -- -240.01+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1110 111+      Hex layout: f7+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.111p+7+           Octal: -0o3.6p+6+         Decimal: -240.0+             Hex: -0xFp+4+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -240.01, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTP_-248.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTP -- -248.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1110 111+      Hex layout: f7+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.111p+7+           Octal: -0o3.6p+6+         Decimal: -240.0+             Hex: -0xFp+4+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -248.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTP_-419.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTP -- -419.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 101+      Hex layout: fd+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.101p+8+           Octal: -0o6.4p+6+         Decimal: -416.0+             Hex: -0x1.Ap+8+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -419.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTP_-432.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTP -- -432.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 101+      Hex layout: fd+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.101p+8+           Octal: -0o6.4p+6+         Decimal: -416.0+             Hex: -0x1.Ap+8+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -432.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTZ_+240.01.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTZ --  240.01+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1110 111+      Hex layout: 77+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.111p+7+           Octal: 0o3.6p+6+         Decimal: 240.0+             Hex: 0xFp+4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 240.01, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTZ_+248.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTZ --  248.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1110 111+      Hex layout: 77+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.111p+7+           Octal: 0o3.6p+6+         Decimal: 240.0+             Hex: 0xFp+4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 248.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTZ_+419.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTZ --  419.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 101+      Hex layout: 7d+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.101p+8+           Octal: 0o6.4p+6+         Decimal: 416.0+             Hex: 0x1.Ap+8+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 419.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTZ_+432.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTZ --  432.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 1111 101+      Hex layout: 7d+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: 0b1.101p+8+           Octal: 0o6.4p+6+         Decimal: 416.0+             Hex: 0x1.Ap+8+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 432.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTZ_-240.01.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTZ -- -240.01+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1110 111+      Hex layout: f7+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.111p+7+           Octal: -0o3.6p+6+         Decimal: -240.0+             Hex: -0xFp+4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -240.01, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTZ_-248.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTZ -- -248.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -240.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1110 111+      Hex layout: f7+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 7 (Stored: 14, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.111p+7+           Octal: -0o3.6p+6+         Decimal: -240.0+             Hex: -0xFp+4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -248.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTZ_-419.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTZ -- -419.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 101+      Hex layout: fd+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.101p+8+           Octal: -0o6.4p+6+         Decimal: -416.0+             Hex: -0x1.Ap+8+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -419.0, represented as E4M3 special value
+ Golds/encodeE4M3_special_RTZ_-432.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe4m3 -rRTZ -- -432.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -416.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 1111 101+      Hex layout: fd+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: 8 (Stored: 15, Bias: 7)+  Classification: FP_NORMAL+          Binary: -0b1.101p+8+           Octal: -0o6.4p+6+         Decimal: -416.0+             Hex: -0x1.Ap+8+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -432.0, represented as E4M3 special value
+ Golds/encodeE4M3_zero1.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 --  0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 0 0000 000+      Hex layout: 00+       Precision: 4 exponent bits, 3 significand bits+            Sign: Positive+        Exponent: -7 (Stored: 0, Bias: 7)+  Classification: FP_ZERO+          Binary: 0b0.0+           Octal: 0o0.0+         Decimal: 0.0+             Hex: 0x0
+ Golds/encodeE4M3_zero2.gold view
@@ -0,0 +1,16 @@+Arguments: -fe4m3 --  -0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0.0 :: E4M3+                  7 6543 210+                  S -E4- S3-+   Binary layout: 1 0000 000+      Hex layout: 80+       Precision: 4 exponent bits, 3 significand bits+            Sign: Negative+        Exponent: -7 (Stored: 0, Bias: 7)+  Classification: FP_ZERO+          Binary: -0b0.0+           Octal: -0o0.0+         Decimal: -0.0+             Hex: -0o0
+ Golds/encodeE8M0_+inf.gold view
@@ -0,0 +1,19 @@+Arguments: -fe8m0    inf+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.7014118346046923e38 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 11111110+      Hex layout: FE+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 127 (Stored: 254, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+127+           Octal: 0o2p+126+         Decimal: 1.7014118346046923e38+             Hex: 0x8p+124+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of Infinity is out of range, saturated to 1.7014118346046923e38.+                  The representable range is [2^-127, 2^127].
+ Golds/encodeE8M0_-inf.gold view
@@ -0,0 +1,7 @@+Arguments: -fe8m0 -- -inf+Exit code: ExitFailure 1++STDERR:+ERROR:+  E8M0 has no representation for negative values.+  The representable range is [2^-127, 2^127], plus NaN.
+ Golds/encodeE8M0_exact.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 --  0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.25 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 01111101+      Hex layout: 7D+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: -2 (Stored: 125, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p-2+           Octal: 0o2p-3+         Decimal: 0.25+             Hex: 0x4p-4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "0.25" was exact. No rounding happened.
+ Golds/encodeE8M0_hex.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 --  0x1.8p1+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000000+      Hex layout: 80+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 3.0 was rounded to 2.0.
+ Golds/encodeE8M0_max.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 --  0x1p+127+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.7014118346046923e38 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 11111110+      Hex layout: FE+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 127 (Stored: 254, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+127+           Octal: 0o2p+126+         Decimal: 1.7014118346046923e38+             Hex: 0x8p+124+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "0x1p+127" was exact. No rounding happened.
+ Golds/encodeE8M0_min.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 --  0x1p-127+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 5.877471754111438e-39 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 00000000+      Hex layout: 00+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: -127 (Stored: 0, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p-127+           Octal: 0o4p-129+         Decimal: 5.877471754111438e-39+             Hex: 0x2p-128+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "0x1p-127" was exact. No rounding happened.
+ Golds/encodeE8M0_nan.gold view
@@ -0,0 +1,15 @@+Arguments: -fe8m0    nan+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: E8M0+                  76543210+                  ---E8---+   Binary layout: 11111111+      Hex layout: FF+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_NAN+           Value: NaN+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "nan" was exact. No rounding happened.
+ Golds/encodeE8M0_neg.gold view
@@ -0,0 +1,7 @@+Arguments: -fe8m0 -- -5+Exit code: ExitFailure 1++STDERR:+ERROR:+  E8M0 has no representation for negative values.+  The representable range is [2^-127, 2^127], plus NaN.
+ Golds/encodeE8M0_one.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 --  1+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 01111111+      Hex layout: 7F+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 0 (Stored: 127, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "1" was exact. No rounding happened.
+ Golds/encodeE8M0_oob1.gold view
@@ -0,0 +1,19 @@+Arguments: -fe8m0 --  1e40+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.7014118346046923e38 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 11111110+      Hex layout: FE+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 127 (Stored: 254, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+127+           Octal: 0o2p+126+         Decimal: 1.7014118346046923e38+             Hex: 0x8p+124+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 1.0e40 is out of range, saturated to 1.7014118346046923e38.+                  The representable range is [2^-127, 2^127].
+ Golds/encodeE8M0_oob2.gold view
@@ -0,0 +1,19 @@+Arguments: -fe8m0 --  1e-40+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 5.877471754111438e-39 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 00000000+      Hex layout: 00+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: -127 (Stored: 0, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p-127+           Octal: 0o4p-129+         Decimal: 5.877471754111438e-39+             Hex: 0x2p-128+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 1.0e-40 is out of range, saturated to 5.877471754111438e-39.+                  The representable range is [2^-127, 2^127].
+ Golds/encodeE8M0_tie_RNA_+0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRNA --  0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 01111111+      Hex layout: 7F+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 0 (Stored: 127, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 0.75 was rounded to 1.0.
+ Golds/encodeE8M0_tie_RNA_+1.5.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRNA --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000000+      Hex layout: 80+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 1.5 was rounded to 2.0.
+ Golds/encodeE8M0_tie_RNA_+3.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRNA --  3.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000001+      Hex layout: 81+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 2 (Stored: 129, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 3.0 was rounded to 4.0.
+ Golds/encodeE8M0_tie_RNA_+6.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRNA --  6.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 8.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000010+      Hex layout: 82+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 3 (Stored: 130, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+3+           Octal: 0o1p+3+         Decimal: 8.0+             Hex: 0x8+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 6.0 was rounded to 8.0.
+ Golds/encodeE8M0_tie_RNE_+0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRNE --  0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.5 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 01111110+      Hex layout: 7E+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: -1 (Stored: 126, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p-1+           Octal: 0o4p-3+         Decimal: 0.5+             Hex: 0x8p-4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 0.75 was rounded to 0.5.
+ Golds/encodeE8M0_tie_RNE_+1.5.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRNE --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000000+      Hex layout: 80+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 1.5 was rounded to 2.0.
+ Golds/encodeE8M0_tie_RNE_+3.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRNE --  3.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000000+      Hex layout: 80+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 3.0 was rounded to 2.0.
+ Golds/encodeE8M0_tie_RNE_+6.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRNE --  6.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 8.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000010+      Hex layout: 82+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 3 (Stored: 130, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+3+           Octal: 0o1p+3+         Decimal: 8.0+             Hex: 0x8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 6.0 was rounded to 8.0.
+ Golds/encodeE8M0_tie_RTN_+0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTN --  0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.5 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 01111110+      Hex layout: 7E+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: -1 (Stored: 126, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p-1+           Octal: 0o4p-3+         Decimal: 0.5+             Hex: 0x8p-4+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 0.75 was rounded to 0.5.
+ Golds/encodeE8M0_tie_RTN_+1.5.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTN --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 01111111+      Hex layout: 7F+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 0 (Stored: 127, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 1.5 was rounded to 1.0.
+ Golds/encodeE8M0_tie_RTN_+3.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTN --  3.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000000+      Hex layout: 80+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 3.0 was rounded to 2.0.
+ Golds/encodeE8M0_tie_RTN_+6.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTN --  6.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000001+      Hex layout: 81+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 2 (Stored: 129, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 6.0 was rounded to 4.0.
+ Golds/encodeE8M0_tie_RTP_+0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTP --  0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 01111111+      Hex layout: 7F+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 0 (Stored: 127, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 0.75 was rounded to 1.0.
+ Golds/encodeE8M0_tie_RTP_+1.5.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTP --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000000+      Hex layout: 80+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 1.5 was rounded to 2.0.
+ Golds/encodeE8M0_tie_RTP_+3.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTP --  3.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000001+      Hex layout: 81+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 2 (Stored: 129, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 3.0 was rounded to 4.0.
+ Golds/encodeE8M0_tie_RTP_+6.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTP --  6.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 8.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000010+      Hex layout: 82+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 3 (Stored: 130, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+3+           Octal: 0o1p+3+         Decimal: 8.0+             Hex: 0x8+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 6.0 was rounded to 8.0.
+ Golds/encodeE8M0_tie_RTZ_+0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTZ --  0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.5 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 01111110+      Hex layout: 7E+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: -1 (Stored: 126, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p-1+           Octal: 0o4p-3+         Decimal: 0.5+             Hex: 0x8p-4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 0.75 was rounded to 0.5.
+ Golds/encodeE8M0_tie_RTZ_+1.5.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTZ --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 01111111+      Hex layout: 7F+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 0 (Stored: 127, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 1.5 was rounded to 1.0.
+ Golds/encodeE8M0_tie_RTZ_+3.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTZ --  3.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000000+      Hex layout: 80+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 1 (Stored: 128, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 3.0 was rounded to 2.0.
+ Golds/encodeE8M0_tie_RTZ_+6.0.gold view
@@ -0,0 +1,18 @@+Arguments: -fe8m0 -rRTZ --  6.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 10000001+      Hex layout: 81+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: 2 (Stored: 129, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 6.0 was rounded to 4.0.
+ Golds/encodeE8M0_zero1.gold view
@@ -0,0 +1,19 @@+Arguments: -fe8m0 --  0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 5.877471754111438e-39 :: E8M0+                  76543210+                  ---E8---+   Binary layout: 00000000+      Hex layout: 00+       Precision: 8 exponent bits, no significand+            Sign: Positive (always)+        Exponent: -127 (Stored: 0, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1p-127+           Octal: 0o4p-129+         Decimal: 5.877471754111438e-39+             Hex: 0x2p-128+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 0.0 is out of range, saturated to 5.877471754111438e-39.+                  The representable range is [2^-127, 2^127].
+ Golds/encodeE8M0_zero2.gold view
@@ -0,0 +1,7 @@+Arguments: -fe8m0 --  -0+Exit code: ExitFailure 1++STDERR:+ERROR:+  E8M0 has no representation for negative values.+  The representable range is [2^-127, 2^127], plus NaN.
+ Golds/encodeFP4E0M3_+inf.gold view
@@ -0,0 +1,7 @@+Arguments: -ffp4e0m3    inf+Exit code: ExitFailure 1++STDERR:+ERROR:+  FP4E0M3 has no representation for infinity.+  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_-inf.gold view
@@ -0,0 +1,7 @@+Arguments: -ffp4e0m3 -- -inf+Exit code: ExitFailure 1++STDERR:+ERROR:+  FP4E0M3 has no representation for infinity.+  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_exact.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 --  5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 101+      Hex layout: 5+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b101+           Octal: 0o5+         Decimal: 5+             Hex: 0x5+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "5" was exact. No rounding happened.
+ Golds/encodeFP4E0M3_hex.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 --  0x1.8p1+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 011+      Hex layout: 3+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b11+           Octal: 0o3+         Decimal: 3+             Hex: 0x3+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "0x1.8p1" was exact. No rounding happened.
+ Golds/encodeFP4E0M3_max.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 --  7+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 111+      Hex layout: 7+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b111+           Octal: 0o7+         Decimal: 7+             Hex: 0x7+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "7" was exact. No rounding happened.
+ Golds/encodeFP4E0M3_min.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -- -7+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 111+      Hex layout: F+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b111+           Octal: -0o7+         Decimal: -7+             Hex: -0x7+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "-7" was exact. No rounding happened.
+ Golds/encodeFP4E0M3_nan.gold view
@@ -0,0 +1,6 @@+Arguments: -ffp4e0m3    nan+Exit code: ExitFailure 1++STDERR:+ERROR:+  FP4E0M3 has no representation for NaN.
+ Golds/encodeFP4E0M3_oob1.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 --  100+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 111+      Hex layout: 7+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b111+           Octal: 0o7+         Decimal: 7+             Hex: 0x7+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 100.0 is out of range, saturated to 7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_oob2.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -- -100+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 111+      Hex layout: F+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b111+           Octal: -0o7+         Decimal: -7+             Hex: -0x7+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -100.0 is out of range, saturated to -7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_rnd1.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 --  0.4+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 000+      Hex layout: 0+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b0+           Octal: 0o0+         Decimal: 0+             Hex: 0x0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 0.4 was rounded to 0.
+ Golds/encodeFP4E0M3_rnd2.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -- -0.4+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 000+      Hex layout: 8+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b0+           Octal: -0o0+         Decimal: -0+             Hex: -0x0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -0.4 was rounded to -0.
+ Golds/encodeFP4E0M3_tie_RNA_+0.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA --  0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 001+      Hex layout: 1+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b1+           Octal: 0o1+         Decimal: 1+             Hex: 0x1+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 0.5 was rounded to 1.
+ Golds/encodeFP4E0M3_tie_RNA_+1.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 010+      Hex layout: 2+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b10+           Octal: 0o2+         Decimal: 2+             Hex: 0x2+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 1.5 was rounded to 2.
+ Golds/encodeFP4E0M3_tie_RNA_+2.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 011+      Hex layout: 3+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b11+           Octal: 0o3+         Decimal: 3+             Hex: 0x3+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 2.5 was rounded to 3.
+ Golds/encodeFP4E0M3_tie_RNA_+3.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA --  3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 100+      Hex layout: 4+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b100+           Octal: 0o4+         Decimal: 4+             Hex: 0x4+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 3.5 was rounded to 4.
+ Golds/encodeFP4E0M3_tie_RNA_+4.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA --  4.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 101+      Hex layout: 5+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b101+           Octal: 0o5+         Decimal: 5+             Hex: 0x5+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 4.5 was rounded to 5.
+ Golds/encodeFP4E0M3_tie_RNA_+5.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA --  5.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 110+      Hex layout: 6+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b110+           Octal: 0o6+         Decimal: 6+             Hex: 0x6+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 5.5 was rounded to 6.
+ Golds/encodeFP4E0M3_tie_RNA_+6.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA --  6.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 111+      Hex layout: 7+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b111+           Octal: 0o7+         Decimal: 7+             Hex: 0x7+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 6.5 was rounded to 7.
+ Golds/encodeFP4E0M3_tie_RNA_+8.0.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -rRNA --  8.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 111+      Hex layout: 7+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b111+           Octal: 0o7+         Decimal: 7+             Hex: 0x7+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 8.0 is out of range, saturated to 7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_tie_RNA_-0.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA -- -0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 001+      Hex layout: 9+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b1+           Octal: -0o1+         Decimal: -1+             Hex: -0x1+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -0.5 was rounded to -1.
+ Golds/encodeFP4E0M3_tie_RNA_-1.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA -- -1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 010+      Hex layout: A+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b10+           Octal: -0o2+         Decimal: -2+             Hex: -0x2+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -1.5 was rounded to -2.
+ Golds/encodeFP4E0M3_tie_RNA_-2.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA -- -2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 011+      Hex layout: B+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b11+           Octal: -0o3+         Decimal: -3+             Hex: -0x3+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -2.5 was rounded to -3.
+ Golds/encodeFP4E0M3_tie_RNA_-3.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA -- -3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 100+      Hex layout: C+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b100+           Octal: -0o4+         Decimal: -4+             Hex: -0x4+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -3.5 was rounded to -4.
+ Golds/encodeFP4E0M3_tie_RNA_-4.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA -- -4.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 101+      Hex layout: D+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b101+           Octal: -0o5+         Decimal: -5+             Hex: -0x5+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -4.5 was rounded to -5.
+ Golds/encodeFP4E0M3_tie_RNA_-5.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA -- -5.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 110+      Hex layout: E+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b110+           Octal: -0o6+         Decimal: -6+             Hex: -0x6+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -5.5 was rounded to -6.
+ Golds/encodeFP4E0M3_tie_RNA_-6.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNA -- -6.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 111+      Hex layout: F+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b111+           Octal: -0o7+         Decimal: -7+             Hex: -0x7+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -6.5 was rounded to -7.
+ Golds/encodeFP4E0M3_tie_RNA_-8.0.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -rRNA -- -8.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 111+      Hex layout: F+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b111+           Octal: -0o7+         Decimal: -7+             Hex: -0x7+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -8.0 is out of range, saturated to -7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_tie_RNE_+0.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE --  0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 000+      Hex layout: 0+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b0+           Octal: 0o0+         Decimal: 0+             Hex: 0x0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 0.5 was rounded to 0.
+ Golds/encodeFP4E0M3_tie_RNE_+1.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 010+      Hex layout: 2+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b10+           Octal: 0o2+         Decimal: 2+             Hex: 0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 1.5 was rounded to 2.
+ Golds/encodeFP4E0M3_tie_RNE_+2.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 010+      Hex layout: 2+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b10+           Octal: 0o2+         Decimal: 2+             Hex: 0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 2.5 was rounded to 2.
+ Golds/encodeFP4E0M3_tie_RNE_+3.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE --  3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 100+      Hex layout: 4+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b100+           Octal: 0o4+         Decimal: 4+             Hex: 0x4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 3.5 was rounded to 4.
+ Golds/encodeFP4E0M3_tie_RNE_+4.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE --  4.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 100+      Hex layout: 4+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b100+           Octal: 0o4+         Decimal: 4+             Hex: 0x4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 4.5 was rounded to 4.
+ Golds/encodeFP4E0M3_tie_RNE_+5.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE --  5.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 110+      Hex layout: 6+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b110+           Octal: 0o6+         Decimal: 6+             Hex: 0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 5.5 was rounded to 6.
+ Golds/encodeFP4E0M3_tie_RNE_+6.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE --  6.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 110+      Hex layout: 6+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b110+           Octal: 0o6+         Decimal: 6+             Hex: 0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 6.5 was rounded to 6.
+ Golds/encodeFP4E0M3_tie_RNE_+8.0.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -rRNE --  8.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 111+      Hex layout: 7+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b111+           Octal: 0o7+         Decimal: 7+             Hex: 0x7+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 8.0 is out of range, saturated to 7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_tie_RNE_-0.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE -- -0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 000+      Hex layout: 8+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b0+           Octal: -0o0+         Decimal: -0+             Hex: -0x0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -0.5 was rounded to -0.
+ Golds/encodeFP4E0M3_tie_RNE_-1.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE -- -1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 010+      Hex layout: A+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b10+           Octal: -0o2+         Decimal: -2+             Hex: -0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -1.5 was rounded to -2.
+ Golds/encodeFP4E0M3_tie_RNE_-2.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE -- -2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 010+      Hex layout: A+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b10+           Octal: -0o2+         Decimal: -2+             Hex: -0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -2.5 was rounded to -2.
+ Golds/encodeFP4E0M3_tie_RNE_-3.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE -- -3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 100+      Hex layout: C+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b100+           Octal: -0o4+         Decimal: -4+             Hex: -0x4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -3.5 was rounded to -4.
+ Golds/encodeFP4E0M3_tie_RNE_-4.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE -- -4.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 100+      Hex layout: C+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b100+           Octal: -0o4+         Decimal: -4+             Hex: -0x4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -4.5 was rounded to -4.
+ Golds/encodeFP4E0M3_tie_RNE_-5.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE -- -5.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 110+      Hex layout: E+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b110+           Octal: -0o6+         Decimal: -6+             Hex: -0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -5.5 was rounded to -6.
+ Golds/encodeFP4E0M3_tie_RNE_-6.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRNE -- -6.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 110+      Hex layout: E+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b110+           Octal: -0o6+         Decimal: -6+             Hex: -0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -6.5 was rounded to -6.
+ Golds/encodeFP4E0M3_tie_RNE_-8.0.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -rRNE -- -8.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 111+      Hex layout: F+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b111+           Octal: -0o7+         Decimal: -7+             Hex: -0x7+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -8.0 is out of range, saturated to -7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_tie_RTN_+0.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN --  0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 000+      Hex layout: 0+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b0+           Octal: 0o0+         Decimal: 0+             Hex: 0x0+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 0.5 was rounded to 0.
+ Golds/encodeFP4E0M3_tie_RTN_+1.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 001+      Hex layout: 1+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b1+           Octal: 0o1+         Decimal: 1+             Hex: 0x1+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 1.5 was rounded to 1.
+ Golds/encodeFP4E0M3_tie_RTN_+2.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 010+      Hex layout: 2+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b10+           Octal: 0o2+         Decimal: 2+             Hex: 0x2+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 2.5 was rounded to 2.
+ Golds/encodeFP4E0M3_tie_RTN_+3.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN --  3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 011+      Hex layout: 3+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b11+           Octal: 0o3+         Decimal: 3+             Hex: 0x3+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 3.5 was rounded to 3.
+ Golds/encodeFP4E0M3_tie_RTN_+4.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN --  4.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 100+      Hex layout: 4+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b100+           Octal: 0o4+         Decimal: 4+             Hex: 0x4+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 4.5 was rounded to 4.
+ Golds/encodeFP4E0M3_tie_RTN_+5.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN --  5.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 101+      Hex layout: 5+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b101+           Octal: 0o5+         Decimal: 5+             Hex: 0x5+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 5.5 was rounded to 5.
+ Golds/encodeFP4E0M3_tie_RTN_+6.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN --  6.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 110+      Hex layout: 6+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b110+           Octal: 0o6+         Decimal: 6+             Hex: 0x6+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 6.5 was rounded to 6.
+ Golds/encodeFP4E0M3_tie_RTN_+8.0.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -rRTN --  8.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 111+      Hex layout: 7+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b111+           Octal: 0o7+         Decimal: 7+             Hex: 0x7+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 8.0 is out of range, saturated to 7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_tie_RTN_-0.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN -- -0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 001+      Hex layout: 9+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b1+           Octal: -0o1+         Decimal: -1+             Hex: -0x1+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -0.5 was rounded to -1.
+ Golds/encodeFP4E0M3_tie_RTN_-1.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN -- -1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 010+      Hex layout: A+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b10+           Octal: -0o2+         Decimal: -2+             Hex: -0x2+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -1.5 was rounded to -2.
+ Golds/encodeFP4E0M3_tie_RTN_-2.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN -- -2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 011+      Hex layout: B+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b11+           Octal: -0o3+         Decimal: -3+             Hex: -0x3+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -2.5 was rounded to -3.
+ Golds/encodeFP4E0M3_tie_RTN_-3.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN -- -3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 100+      Hex layout: C+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b100+           Octal: -0o4+         Decimal: -4+             Hex: -0x4+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -3.5 was rounded to -4.
+ Golds/encodeFP4E0M3_tie_RTN_-4.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN -- -4.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 101+      Hex layout: D+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b101+           Octal: -0o5+         Decimal: -5+             Hex: -0x5+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -4.5 was rounded to -5.
+ Golds/encodeFP4E0M3_tie_RTN_-5.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN -- -5.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 110+      Hex layout: E+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b110+           Octal: -0o6+         Decimal: -6+             Hex: -0x6+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -5.5 was rounded to -6.
+ Golds/encodeFP4E0M3_tie_RTN_-6.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTN -- -6.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 111+      Hex layout: F+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b111+           Octal: -0o7+         Decimal: -7+             Hex: -0x7+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -6.5 was rounded to -7.
+ Golds/encodeFP4E0M3_tie_RTN_-8.0.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -rRTN -- -8.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 111+      Hex layout: F+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b111+           Octal: -0o7+         Decimal: -7+             Hex: -0x7+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -8.0 is out of range, saturated to -7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_tie_RTP_+0.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP --  0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 001+      Hex layout: 1+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b1+           Octal: 0o1+         Decimal: 1+             Hex: 0x1+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 0.5 was rounded to 1.
+ Golds/encodeFP4E0M3_tie_RTP_+1.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 010+      Hex layout: 2+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b10+           Octal: 0o2+         Decimal: 2+             Hex: 0x2+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 1.5 was rounded to 2.
+ Golds/encodeFP4E0M3_tie_RTP_+2.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 011+      Hex layout: 3+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b11+           Octal: 0o3+         Decimal: 3+             Hex: 0x3+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 2.5 was rounded to 3.
+ Golds/encodeFP4E0M3_tie_RTP_+3.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP --  3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 100+      Hex layout: 4+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b100+           Octal: 0o4+         Decimal: 4+             Hex: 0x4+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 3.5 was rounded to 4.
+ Golds/encodeFP4E0M3_tie_RTP_+4.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP --  4.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 101+      Hex layout: 5+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b101+           Octal: 0o5+         Decimal: 5+             Hex: 0x5+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 4.5 was rounded to 5.
+ Golds/encodeFP4E0M3_tie_RTP_+5.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP --  5.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 110+      Hex layout: 6+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b110+           Octal: 0o6+         Decimal: 6+             Hex: 0x6+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 5.5 was rounded to 6.
+ Golds/encodeFP4E0M3_tie_RTP_+6.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP --  6.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 111+      Hex layout: 7+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b111+           Octal: 0o7+         Decimal: 7+             Hex: 0x7+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 6.5 was rounded to 7.
+ Golds/encodeFP4E0M3_tie_RTP_+8.0.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -rRTP --  8.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 111+      Hex layout: 7+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b111+           Octal: 0o7+         Decimal: 7+             Hex: 0x7+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 8.0 is out of range, saturated to 7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_tie_RTP_-0.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP -- -0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 000+      Hex layout: 8+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b0+           Octal: -0o0+         Decimal: -0+             Hex: -0x0+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -0.5 was rounded to -0.
+ Golds/encodeFP4E0M3_tie_RTP_-1.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP -- -1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 001+      Hex layout: 9+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b1+           Octal: -0o1+         Decimal: -1+             Hex: -0x1+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -1.5 was rounded to -1.
+ Golds/encodeFP4E0M3_tie_RTP_-2.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP -- -2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 010+      Hex layout: A+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b10+           Octal: -0o2+         Decimal: -2+             Hex: -0x2+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -2.5 was rounded to -2.
+ Golds/encodeFP4E0M3_tie_RTP_-3.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP -- -3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 011+      Hex layout: B+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b11+           Octal: -0o3+         Decimal: -3+             Hex: -0x3+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -3.5 was rounded to -3.
+ Golds/encodeFP4E0M3_tie_RTP_-4.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP -- -4.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 100+      Hex layout: C+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b100+           Octal: -0o4+         Decimal: -4+             Hex: -0x4+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -4.5 was rounded to -4.
+ Golds/encodeFP4E0M3_tie_RTP_-5.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP -- -5.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 101+      Hex layout: D+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b101+           Octal: -0o5+         Decimal: -5+             Hex: -0x5+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -5.5 was rounded to -5.
+ Golds/encodeFP4E0M3_tie_RTP_-6.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTP -- -6.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 110+      Hex layout: E+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b110+           Octal: -0o6+         Decimal: -6+             Hex: -0x6+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -6.5 was rounded to -6.
+ Golds/encodeFP4E0M3_tie_RTP_-8.0.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -rRTP -- -8.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 111+      Hex layout: F+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b111+           Octal: -0o7+         Decimal: -7+             Hex: -0x7+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -8.0 is out of range, saturated to -7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_tie_RTZ_+0.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ --  0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 000+      Hex layout: 0+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b0+           Octal: 0o0+         Decimal: 0+             Hex: 0x0+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 0.5 was rounded to 0.
+ Golds/encodeFP4E0M3_tie_RTZ_+1.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 001+      Hex layout: 1+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b1+           Octal: 0o1+         Decimal: 1+             Hex: 0x1+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 1.5 was rounded to 1.
+ Golds/encodeFP4E0M3_tie_RTZ_+2.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 010+      Hex layout: 2+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b10+           Octal: 0o2+         Decimal: 2+             Hex: 0x2+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 2.5 was rounded to 2.
+ Golds/encodeFP4E0M3_tie_RTZ_+3.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ --  3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 011+      Hex layout: 3+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b11+           Octal: 0o3+         Decimal: 3+             Hex: 0x3+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 3.5 was rounded to 3.
+ Golds/encodeFP4E0M3_tie_RTZ_+4.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ --  4.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 100+      Hex layout: 4+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b100+           Octal: 0o4+         Decimal: 4+             Hex: 0x4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 4.5 was rounded to 4.
+ Golds/encodeFP4E0M3_tie_RTZ_+5.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ --  5.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 101+      Hex layout: 5+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b101+           Octal: 0o5+         Decimal: 5+             Hex: 0x5+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 5.5 was rounded to 5.
+ Golds/encodeFP4E0M3_tie_RTZ_+6.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ --  6.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 110+      Hex layout: 6+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b110+           Octal: 0o6+         Decimal: 6+             Hex: 0x6+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 6.5 was rounded to 6.
+ Golds/encodeFP4E0M3_tie_RTZ_+8.0.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -rRTZ --  8.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 111+      Hex layout: 7+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b111+           Octal: 0o7+         Decimal: 7+             Hex: 0x7+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 8.0 is out of range, saturated to 7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_tie_RTZ_-0.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ -- -0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 000+      Hex layout: 8+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b0+           Octal: -0o0+         Decimal: -0+             Hex: -0x0+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -0.5 was rounded to -0.
+ Golds/encodeFP4E0M3_tie_RTZ_-1.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ -- -1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 001+      Hex layout: 9+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b1+           Octal: -0o1+         Decimal: -1+             Hex: -0x1+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -1.5 was rounded to -1.
+ Golds/encodeFP4E0M3_tie_RTZ_-2.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ -- -2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 010+      Hex layout: A+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b10+           Octal: -0o2+         Decimal: -2+             Hex: -0x2+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -2.5 was rounded to -2.
+ Golds/encodeFP4E0M3_tie_RTZ_-3.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ -- -3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -3 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 011+      Hex layout: B+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b11+           Octal: -0o3+         Decimal: -3+             Hex: -0x3+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -3.5 was rounded to -3.
+ Golds/encodeFP4E0M3_tie_RTZ_-4.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ -- -4.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 100+      Hex layout: C+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b100+           Octal: -0o4+         Decimal: -4+             Hex: -0x4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -4.5 was rounded to -4.
+ Golds/encodeFP4E0M3_tie_RTZ_-5.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ -- -5.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -5 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 101+      Hex layout: D+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b101+           Octal: -0o5+         Decimal: -5+             Hex: -0x5+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -5.5 was rounded to -5.
+ Golds/encodeFP4E0M3_tie_RTZ_-6.5.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 -rRTZ -- -6.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 110+      Hex layout: E+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b110+           Octal: -0o6+         Decimal: -6+             Hex: -0x6+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -6.5 was rounded to -6.
+ Golds/encodeFP4E0M3_tie_RTZ_-8.0.gold view
@@ -0,0 +1,17 @@+Arguments: -ffp4e0m3 -rRTZ -- -8.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -7 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 111+      Hex layout: F+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b111+           Octal: -0o7+         Decimal: -7+             Hex: -0x7+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -8.0 is out of range, saturated to -7.+                  The representable range is [-7, 7].
+ Golds/encodeFP4E0M3_zero1.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 --  0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 0 000+      Hex layout: 0+            Type: 4-bit sign-magnitude integer+            Sign: Positive+          Binary: 0b0+           Octal: 0o0+         Decimal: 0+             Hex: 0x0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "0" was exact. No rounding happened.
+ Golds/encodeFP4E0M3_zero2.gold view
@@ -0,0 +1,16 @@+Arguments: -ffp4e0m3 --  -0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0 :: FP4E0M3+                  3 210+                  S -M-+   Binary layout: 1 000+      Hex layout: 8+            Type: 4-bit sign-magnitude integer+            Sign: Negative+          Binary: -0b0+           Octal: -0o0+         Decimal: -0+             Hex: -0x0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "-0" was exact. No rounding happened.
+ Golds/encodeFP4_+inf.gold view
@@ -0,0 +1,7 @@+Arguments: -ffp4    inf+Exit code: ExitFailure 1++STDERR:+ERROR:+  FP4 has no representation for infinity.+  The representable range is [-6, 6].
+ Golds/encodeFP4_-inf.gold view
@@ -0,0 +1,7 @@+Arguments: -ffp4 -- -inf+Exit code: ExitFailure 1++STDERR:+ERROR:+  FP4 has no representation for infinity.+  The representable range is [-6, 6].
+ Golds/encodeFP4_dev1.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 --  4+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 0+      Hex layout: 6+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "4" was exact. No rounding happened.
+ Golds/encodeFP4_dev2.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 --  6+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "6" was exact. No rounding happened.
+ Golds/encodeFP4_dev3.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -- -6+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 1+      Hex layout: F+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p+2+           Octal: -0o6+         Decimal: -6.0+             Hex: -0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "-6" was exact. No rounding happened.
+ Golds/encodeFP4_hex.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 --  0x1.8p2+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "0x1.8p2" was exact. No rounding happened.
+ Golds/encodeFP4_nan.gold view
@@ -0,0 +1,6 @@+Arguments: -ffp4    nan+Exit code: ExitFailure 1++STDERR:+ERROR:+  FP4 has no representation for NaN.
+ Golds/encodeFP4_norm.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 --  1.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 1+      Hex layout: 3+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1+           Octal: 0o1.4+         Decimal: 1.5+             Hex: 0x1.8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "1.5" was exact. No rounding happened.
+ Golds/encodeFP4_oob1.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 --  100+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 100.0 is out of range, saturated to 6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_oob2.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -- -100+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 1+      Hex layout: F+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p+2+           Octal: -0o6+         Decimal: -6.0+             Hex: -0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -100.0 is out of range, saturated to -6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_sub.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 --  0.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 1+      Hex layout: 1+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: 0b1p-1+           Octal: 0o4p-3+         Decimal: 0.5+             Hex: 0x8p-4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "0.5" was exact. No rounding happened.
+ Golds/encodeFP4_tie_RNA_+0.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA --  0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 1+      Hex layout: 1+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: 0b1p-1+           Octal: 0o4p-3+         Decimal: 0.5+             Hex: 0x8p-4+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 0.25 was rounded to 0.5.
+ Golds/encodeFP4_tie_RNA_+0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA --  0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 0+      Hex layout: 2+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 0.75 was rounded to 1.0.
+ Golds/encodeFP4_tie_RNA_+1.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA --  1.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 1+      Hex layout: 3+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1+           Octal: 0o1.4+         Decimal: 1.5+             Hex: 0x1.8+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 1.25 was rounded to 1.5.
+ Golds/encodeFP4_tie_RNA_+1.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA --  1.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 0+      Hex layout: 4+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 1.75 was rounded to 2.0.
+ Golds/encodeFP4_tie_RNA_+2.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 3.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 1+      Hex layout: 5+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p1+           Octal: 0o3+         Decimal: 3.0+             Hex: 0x3+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 2.5 was rounded to 3.0.
+ Golds/encodeFP4_tie_RNA_+3.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA --  3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 0+      Hex layout: 6+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 3.5 was rounded to 4.0.
+ Golds/encodeFP4_tie_RNA_+5.0.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA --  5.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 5.0 was rounded to 6.0.
+ Golds/encodeFP4_tie_RNA_+7.0.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -rRNA --  7.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 7.0 is out of range, saturated to 6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_tie_RNA_-0.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA -- -0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 00 1+      Hex layout: 9+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: -0b1p-1+           Octal: -0o4p-3+         Decimal: -0.5+             Hex: -0x8p-4+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -0.25 was rounded to -0.5.
+ Golds/encodeFP4_tie_RNA_-0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA -- -0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 0+      Hex layout: A+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1+           Octal: -0o1+         Decimal: -1.0+             Hex: -0x1+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -0.75 was rounded to -1.0.
+ Golds/encodeFP4_tie_RNA_-1.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA -- -1.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 1+      Hex layout: B+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1+           Octal: -0o1.4+         Decimal: -1.5+             Hex: -0x1.8+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -1.25 was rounded to -1.5.
+ Golds/encodeFP4_tie_RNA_-1.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA -- -1.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 0+      Hex layout: C+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p1+           Octal: -0o2+         Decimal: -2.0+             Hex: -0x2+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -1.75 was rounded to -2.0.
+ Golds/encodeFP4_tie_RNA_-2.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA -- -2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -3.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 1+      Hex layout: D+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p1+           Octal: -0o3+         Decimal: -3.0+             Hex: -0x3+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -2.5 was rounded to -3.0.
+ Golds/encodeFP4_tie_RNA_-3.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA -- -3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 0+      Hex layout: E+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p+2+           Octal: -0o4+         Decimal: -4.0+             Hex: -0x4+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -3.5 was rounded to -4.0.
+ Golds/encodeFP4_tie_RNA_-5.0.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNA -- -5.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 1+      Hex layout: F+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p+2+           Octal: -0o6+         Decimal: -6.0+             Hex: -0x6+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -5.0 was rounded to -6.0.
+ Golds/encodeFP4_tie_RNA_-7.0.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -rRNA -- -7.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 1+      Hex layout: F+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p+2+           Octal: -0o6+         Decimal: -6.0+             Hex: -0x6+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of -7.0 is out of range, saturated to -6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_tie_RNE_+0.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE --  0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 0+      Hex layout: 0+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: -1 (Stored: 0, Bias: 1)+  Classification: FP_ZERO+          Binary: 0b0.0+           Octal: 0o0.0+         Decimal: 0.0+             Hex: 0x0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 0.25 was rounded to 0.0.
+ Golds/encodeFP4_tie_RNE_+0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE --  0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 0+      Hex layout: 2+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 0.75 was rounded to 1.0.
+ Golds/encodeFP4_tie_RNE_+1.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE --  1.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 0+      Hex layout: 2+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 1.25 was rounded to 1.0.
+ Golds/encodeFP4_tie_RNE_+1.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE --  1.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 0+      Hex layout: 4+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 1.75 was rounded to 2.0.
+ Golds/encodeFP4_tie_RNE_+2.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 0+      Hex layout: 4+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 2.5 was rounded to 2.0.
+ Golds/encodeFP4_tie_RNE_+3.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE --  3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 0+      Hex layout: 6+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 3.5 was rounded to 4.0.
+ Golds/encodeFP4_tie_RNE_+5.0.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE --  5.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 0+      Hex layout: 6+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 5.0 was rounded to 4.0.
+ Golds/encodeFP4_tie_RNE_+7.0.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -rRNE --  7.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 7.0 is out of range, saturated to 6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_tie_RNE_-0.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE -- -0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 00 0+      Hex layout: 8+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: -1 (Stored: 0, Bias: 1)+  Classification: FP_ZERO+          Binary: -0b0.0+           Octal: -0o0.0+         Decimal: -0.0+             Hex: -0o0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -0.25 was rounded to -0.0.
+ Golds/encodeFP4_tie_RNE_-0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE -- -0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 0+      Hex layout: A+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1+           Octal: -0o1+         Decimal: -1.0+             Hex: -0x1+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -0.75 was rounded to -1.0.
+ Golds/encodeFP4_tie_RNE_-1.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE -- -1.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 0+      Hex layout: A+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1+           Octal: -0o1+         Decimal: -1.0+             Hex: -0x1+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -1.25 was rounded to -1.0.
+ Golds/encodeFP4_tie_RNE_-1.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE -- -1.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 0+      Hex layout: C+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p1+           Octal: -0o2+         Decimal: -2.0+             Hex: -0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -1.75 was rounded to -2.0.
+ Golds/encodeFP4_tie_RNE_-2.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE -- -2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 0+      Hex layout: C+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p1+           Octal: -0o2+         Decimal: -2.0+             Hex: -0x2+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -2.5 was rounded to -2.0.
+ Golds/encodeFP4_tie_RNE_-3.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE -- -3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 0+      Hex layout: E+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p+2+           Octal: -0o4+         Decimal: -4.0+             Hex: -0x4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -3.5 was rounded to -4.0.
+ Golds/encodeFP4_tie_RNE_-5.0.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRNE -- -5.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 0+      Hex layout: E+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p+2+           Octal: -0o4+         Decimal: -4.0+             Hex: -0x4+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -5.0 was rounded to -4.0.
+ Golds/encodeFP4_tie_RNE_-7.0.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -rRNE -- -7.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 1+      Hex layout: F+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p+2+           Octal: -0o6+         Decimal: -6.0+             Hex: -0x6+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of -7.0 is out of range, saturated to -6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_tie_RTN_+0.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN --  0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 0+      Hex layout: 0+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: -1 (Stored: 0, Bias: 1)+  Classification: FP_ZERO+          Binary: 0b0.0+           Octal: 0o0.0+         Decimal: 0.0+             Hex: 0x0+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 0.25 was rounded to 0.0.
+ Golds/encodeFP4_tie_RTN_+0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN --  0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 1+      Hex layout: 1+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: 0b1p-1+           Octal: 0o4p-3+         Decimal: 0.5+             Hex: 0x8p-4+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 0.75 was rounded to 0.5.
+ Golds/encodeFP4_tie_RTN_+1.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN --  1.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 0+      Hex layout: 2+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 1.25 was rounded to 1.0.
+ Golds/encodeFP4_tie_RTN_+1.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN --  1.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 1+      Hex layout: 3+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1+           Octal: 0o1.4+         Decimal: 1.5+             Hex: 0x1.8+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 1.75 was rounded to 1.5.
+ Golds/encodeFP4_tie_RTN_+2.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 0+      Hex layout: 4+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 2.5 was rounded to 2.0.
+ Golds/encodeFP4_tie_RTN_+3.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN --  3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 3.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 1+      Hex layout: 5+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p1+           Octal: 0o3+         Decimal: 3.0+             Hex: 0x3+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 3.5 was rounded to 3.0.
+ Golds/encodeFP4_tie_RTN_+5.0.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN --  5.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 0+      Hex layout: 6+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 5.0 was rounded to 4.0.
+ Golds/encodeFP4_tie_RTN_+7.0.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -rRTN --  7.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of 7.0 is out of range, saturated to 6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_tie_RTN_-0.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN -- -0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 00 1+      Hex layout: 9+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: -0b1p-1+           Octal: -0o4p-3+         Decimal: -0.5+             Hex: -0x8p-4+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -0.25 was rounded to -0.5.
+ Golds/encodeFP4_tie_RTN_-0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN -- -0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 0+      Hex layout: A+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1+           Octal: -0o1+         Decimal: -1.0+             Hex: -0x1+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -0.75 was rounded to -1.0.
+ Golds/encodeFP4_tie_RTN_-1.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN -- -1.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 1+      Hex layout: B+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1+           Octal: -0o1.4+         Decimal: -1.5+             Hex: -0x1.8+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -1.25 was rounded to -1.5.
+ Golds/encodeFP4_tie_RTN_-1.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN -- -1.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 0+      Hex layout: C+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p1+           Octal: -0o2+         Decimal: -2.0+             Hex: -0x2+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -1.75 was rounded to -2.0.
+ Golds/encodeFP4_tie_RTN_-2.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN -- -2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -3.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 1+      Hex layout: D+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p1+           Octal: -0o3+         Decimal: -3.0+             Hex: -0x3+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -2.5 was rounded to -3.0.
+ Golds/encodeFP4_tie_RTN_-3.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN -- -3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 0+      Hex layout: E+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p+2+           Octal: -0o4+         Decimal: -4.0+             Hex: -0x4+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -3.5 was rounded to -4.0.
+ Golds/encodeFP4_tie_RTN_-5.0.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTN -- -5.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 1+      Hex layout: F+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p+2+           Octal: -0o6+         Decimal: -6.0+             Hex: -0x6+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -5.0 was rounded to -6.0.
+ Golds/encodeFP4_tie_RTN_-7.0.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -rRTN -- -7.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 1+      Hex layout: F+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p+2+           Octal: -0o6+         Decimal: -6.0+             Hex: -0x6+   Rounding mode: RTN: Round towards negative infinity.+            Note: Original value of -7.0 is out of range, saturated to -6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_tie_RTP_+0.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP --  0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 1+      Hex layout: 1+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: 0b1p-1+           Octal: 0o4p-3+         Decimal: 0.5+             Hex: 0x8p-4+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 0.25 was rounded to 0.5.
+ Golds/encodeFP4_tie_RTP_+0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP --  0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 0+      Hex layout: 2+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 0.75 was rounded to 1.0.
+ Golds/encodeFP4_tie_RTP_+1.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP --  1.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 1+      Hex layout: 3+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1+           Octal: 0o1.4+         Decimal: 1.5+             Hex: 0x1.8+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 1.25 was rounded to 1.5.
+ Golds/encodeFP4_tie_RTP_+1.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP --  1.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 0+      Hex layout: 4+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 1.75 was rounded to 2.0.
+ Golds/encodeFP4_tie_RTP_+2.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 3.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 1+      Hex layout: 5+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p1+           Octal: 0o3+         Decimal: 3.0+             Hex: 0x3+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 2.5 was rounded to 3.0.
+ Golds/encodeFP4_tie_RTP_+3.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP --  3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 0+      Hex layout: 6+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 3.5 was rounded to 4.0.
+ Golds/encodeFP4_tie_RTP_+5.0.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP --  5.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 5.0 was rounded to 6.0.
+ Golds/encodeFP4_tie_RTP_+7.0.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -rRTP --  7.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of 7.0 is out of range, saturated to 6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_tie_RTP_-0.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP -- -0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 00 0+      Hex layout: 8+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: -1 (Stored: 0, Bias: 1)+  Classification: FP_ZERO+          Binary: -0b0.0+           Octal: -0o0.0+         Decimal: -0.0+             Hex: -0o0+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -0.25 was rounded to -0.0.
+ Golds/encodeFP4_tie_RTP_-0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP -- -0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 00 1+      Hex layout: 9+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: -0b1p-1+           Octal: -0o4p-3+         Decimal: -0.5+             Hex: -0x8p-4+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -0.75 was rounded to -0.5.
+ Golds/encodeFP4_tie_RTP_-1.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP -- -1.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 0+      Hex layout: A+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1+           Octal: -0o1+         Decimal: -1.0+             Hex: -0x1+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -1.25 was rounded to -1.0.
+ Golds/encodeFP4_tie_RTP_-1.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP -- -1.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 1+      Hex layout: B+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1+           Octal: -0o1.4+         Decimal: -1.5+             Hex: -0x1.8+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -1.75 was rounded to -1.5.
+ Golds/encodeFP4_tie_RTP_-2.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP -- -2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 0+      Hex layout: C+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p1+           Octal: -0o2+         Decimal: -2.0+             Hex: -0x2+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -2.5 was rounded to -2.0.
+ Golds/encodeFP4_tie_RTP_-3.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP -- -3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -3.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 1+      Hex layout: D+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p1+           Octal: -0o3+         Decimal: -3.0+             Hex: -0x3+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -3.5 was rounded to -3.0.
+ Golds/encodeFP4_tie_RTP_-5.0.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTP -- -5.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 0+      Hex layout: E+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p+2+           Octal: -0o4+         Decimal: -4.0+             Hex: -0x4+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -5.0 was rounded to -4.0.
+ Golds/encodeFP4_tie_RTP_-7.0.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -rRTP -- -7.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 1+      Hex layout: F+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p+2+           Octal: -0o6+         Decimal: -6.0+             Hex: -0x6+   Rounding mode: RTP: Round towards positive infinity.+            Note: Original value of -7.0 is out of range, saturated to -6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_tie_RTZ_+0.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ --  0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 0+      Hex layout: 0+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: -1 (Stored: 0, Bias: 1)+  Classification: FP_ZERO+          Binary: 0b0.0+           Octal: 0o0.0+         Decimal: 0.0+             Hex: 0x0+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 0.25 was rounded to 0.0.
+ Golds/encodeFP4_tie_RTZ_+0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ --  0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 1+      Hex layout: 1+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: 0b1p-1+           Octal: 0o4p-3+         Decimal: 0.5+             Hex: 0x8p-4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 0.75 was rounded to 0.5.
+ Golds/encodeFP4_tie_RTZ_+1.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ --  1.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 0+      Hex layout: 2+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 1.25 was rounded to 1.0.
+ Golds/encodeFP4_tie_RTZ_+1.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ --  1.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 01 1+      Hex layout: 3+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1+           Octal: 0o1.4+         Decimal: 1.5+             Hex: 0x1.8+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 1.75 was rounded to 1.5.
+ Golds/encodeFP4_tie_RTZ_+2.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 0+      Hex layout: 4+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 2.5 was rounded to 2.0.
+ Golds/encodeFP4_tie_RTZ_+3.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ --  3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 3.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 10 1+      Hex layout: 5+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p1+           Octal: 0o3+         Decimal: 3.0+             Hex: 0x3+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 3.5 was rounded to 3.0.
+ Golds/encodeFP4_tie_RTZ_+5.0.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ --  5.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 0+      Hex layout: 6+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1p+2+           Octal: 0o4+         Decimal: 4.0+             Hex: 0x4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 5.0 was rounded to 4.0.
+ Golds/encodeFP4_tie_RTZ_+7.0.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -rRTZ --  7.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 11 1+      Hex layout: 7+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: 0b1.1p+2+           Octal: 0o6+         Decimal: 6.0+             Hex: 0x6+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of 7.0 is out of range, saturated to 6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_tie_RTZ_-0.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ -- -0.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 00 0+      Hex layout: 8+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: -1 (Stored: 0, Bias: 1)+  Classification: FP_ZERO+          Binary: -0b0.0+           Octal: -0o0.0+         Decimal: -0.0+             Hex: -0o0+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -0.25 was rounded to -0.0.
+ Golds/encodeFP4_tie_RTZ_-0.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ -- -0.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 00 1+      Hex layout: 9+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Subnormal, with fixed exponent value. Stored: 0, Bias: 1)+  Classification: FP_SUBNORMAL+          Binary: -0b1p-1+           Octal: -0o4p-3+         Decimal: -0.5+             Hex: -0x8p-4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -0.75 was rounded to -0.5.
+ Golds/encodeFP4_tie_RTZ_-1.25.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ -- -1.25+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 0+      Hex layout: A+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1+           Octal: -0o1+         Decimal: -1.0+             Hex: -0x1+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -1.25 was rounded to -1.0.
+ Golds/encodeFP4_tie_RTZ_-1.75.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ -- -1.75+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -1.5 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 01 1+      Hex layout: B+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 0 (Stored: 1, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1+           Octal: -0o1.4+         Decimal: -1.5+             Hex: -0x1.8+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -1.75 was rounded to -1.5.
+ Golds/encodeFP4_tie_RTZ_-2.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ -- -2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -2.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 0+      Hex layout: C+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p1+           Octal: -0o2+         Decimal: -2.0+             Hex: -0x2+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -2.5 was rounded to -2.0.
+ Golds/encodeFP4_tie_RTZ_-3.5.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ -- -3.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -3.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 10 1+      Hex layout: D+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 1 (Stored: 2, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p1+           Octal: -0o3+         Decimal: -3.0+             Hex: -0x3+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -3.5 was rounded to -3.0.
+ Golds/encodeFP4_tie_RTZ_-5.0.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 -rRTZ -- -5.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -4.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 0+      Hex layout: E+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1p+2+           Octal: -0o4+         Decimal: -4.0+             Hex: -0x4+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -5.0 was rounded to -4.0.
+ Golds/encodeFP4_tie_RTZ_-7.0.gold view
@@ -0,0 +1,19 @@+Arguments: -ffp4 -rRTZ -- -7.0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -6.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 11 1+      Hex layout: F+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: 2 (Stored: 3, Bias: 1)+  Classification: FP_NORMAL+          Binary: -0b1.1p+2+           Octal: -0o6+         Decimal: -6.0+             Hex: -0x6+   Rounding mode: RTZ: Round towards zero.+            Note: Original value of -7.0 is out of range, saturated to -6.0.+                  The representable range is [-6, 6].
+ Golds/encodeFP4_zero1.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 --  0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 0 00 0+      Hex layout: 0+       Precision: 2 exponent bits, 1 significand bit+            Sign: Positive+        Exponent: -1 (Stored: 0, Bias: 1)+  Classification: FP_ZERO+          Binary: 0b0.0+           Octal: 0o0.0+         Decimal: 0.0+             Hex: 0x0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "0" was exact. No rounding happened.
+ Golds/encodeFP4_zero2.gold view
@@ -0,0 +1,18 @@+Arguments: -ffp4 --  -0+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = -0.0 :: FP4+                  3 21 0+                  S E2 S+   Binary layout: 1 00 0+      Hex layout: 8+       Precision: 2 exponent bits, 1 significand bit+            Sign: Negative+        Exponent: -1 (Stored: 0, Bias: 1)+  Classification: FP_ZERO+          Binary: -0b0.0+           Octal: -0o0.0+         Decimal: -0.0+             Hex: -0o0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "-0" was exact. No rounding happened.
+ Golds/encodeUE5M3_+inf.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3    inf+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 111+      Hex layout: FF+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NAN+           Value: NaN+   Rounding mode: RNE: Round nearest ties to even.+            Note: The input value Infinity is out of bounds, and hence becomes NaN.+                  The representable range is [0, 114688].
+ Golds/encodeUE5M3_-inf.gold view
@@ -0,0 +1,7 @@+Arguments: -fue5m3 -- -inf+Exit code: ExitFailure 1++STDERR:+ERROR:+  UE5M3 has no representation for negative values.+  The representable range is [0, 114688], plus NaN.
+ Golds/encodeUE5M3_dev.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 --  65536+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 65536.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 000+      Hex layout: F8+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1p+16+           Octal: 0o2p+15+         Decimal: 65536.0+             Hex: 0x1p+16+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "65536" was exact. No rounding happened.
+ Golds/encodeUE5M3_exact.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 --  2.5+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.5 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 10000 010+      Hex layout: 82+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 1 (Stored: 16, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.01p1+           Octal: 0o2.4+         Decimal: 2.5+             Hex: 0x2.8+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "2.5" was exact. No rounding happened.
+ Golds/encodeUE5M3_hex.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 --  0x1.8p1+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 3.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 10000 100+      Hex layout: 84+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 1 (Stored: 16, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.1p1+           Octal: 0o3+         Decimal: 3.0+             Hex: 0x3+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "0x1.8p1" was exact. No rounding happened.
+ Golds/encodeUE5M3_ieeemax.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 --  61440+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 61440 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11110 111+      Hex layout: F7+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 15 (Stored: 30, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.111p15+           Octal: 0o1.7p15+         Decimal: 61440+             Hex: 0xfp12+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "61440" was exact. No rounding happened.
+ Golds/encodeUE5M3_ieeernd.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 --  61441+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 61440 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11110 111+      Hex layout: F7+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 15 (Stored: 30, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.111p15+           Octal: 0o1.7p15+         Decimal: 61440+             Hex: 0xfp12+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 61441.0 was rounded to 61440.0.
+ Golds/encodeUE5M3_max.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 --  114688+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 114688.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 110+      Hex layout: FE+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.11p+16+           Octal: 0o3.4p+15+         Decimal: 114688.0+             Hex: 0x1.cp+16+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "114688" was exact. No rounding happened.
+ Golds/encodeUE5M3_nan.gold view
@@ -0,0 +1,15 @@+Arguments: -fue5m3    nan+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 111+      Hex layout: FF+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NAN+           Value: NaN+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "nan" was exact. No rounding happened.
+ Golds/encodeUE5M3_neg.gold view
@@ -0,0 +1,7 @@+Arguments: -fue5m3 -- -5+Exit code: ExitFailure 1++STDERR:+ERROR:+  UE5M3 has no representation for negative values.+  The representable range is [0, 114688], plus NaN.
+ Golds/encodeUE5M3_one.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 --  1+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 01111 000+      Hex layout: 78+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 0 (Stored: 15, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1+           Octal: 0o1+         Decimal: 1.0+             Hex: 0x1+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "1" was exact. No rounding happened.
+ Golds/encodeUE5M3_oob.gold view
@@ -0,0 +1,16 @@+Arguments: -fue5m3 --  114689+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = NaN :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 111+      Hex layout: FF+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NAN+           Value: NaN+   Rounding mode: RNE: Round nearest ties to even.+            Note: The input value 114689.0 is out of bounds, and hence becomes NaN.+                  The representable range is [0, 114688].
+ Golds/encodeUE5M3_sub.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 --  0x1p-17+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.000007629 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 00000 001+      Hex layout: 01+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: -14 (Subnormal, with fixed exponent value. Stored: 0, Bias: 15)+  Classification: FP_SUBNORMAL+          Binary: 0b1p-17+           Octal: 0o2p-18+         Decimal: 0.000007629+             Hex: 0x8p-20+   Rounding mode: RNE: Round nearest ties to even.+            Note: Conversion from "0x1p-17" was exact. No rounding happened.
+ Golds/encodeUE5M3_subrnd.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 --  1e-10+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 0.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 00000 000+      Hex layout: 00+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: -15 (Stored: 0, Bias: 15)+  Classification: FP_ZERO+          Binary: 0b0.0+           Octal: 0o0.0+         Decimal: 0.0+             Hex: 0x0+   Rounding mode: RNE: Round nearest ties to even.+            Note: Original value of 1.0e-10 was rounded to 0.0.
+ Golds/encodeUE5M3_tie_RNA_binade.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 -rRNA -- 1.9375+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 2.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 10000 000+      Hex layout: 80+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 1 (Stored: 16, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1p1+           Octal: 0o2+         Decimal: 2.0+             Hex: 0x2+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 1.9375 was rounded to 2.0.
+ Golds/encodeUE5M3_tie_RNA_dev0.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 -rRNA -- 63488+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 65536.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 000+      Hex layout: F8+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1p+16+           Octal: 0o2p+15+         Decimal: 65536.0+             Hex: 0x1p+16+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 63488.0 was rounded to 65536.0.
+ Golds/encodeUE5M3_tie_RNA_dev1.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 -rRNA -- 69632+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 73728.0 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 11111 001+      Hex layout: F9+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 16 (Stored: 31, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.001p+16+           Octal: 0o2.2p+15+         Decimal: 73728.0+             Hex: 0x1.2p+16+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 69632.0 was rounded to 73728.0.
+ Golds/encodeUE5M3_tie_RNA_norm.gold view
@@ -0,0 +1,18 @@+Arguments: -fue5m3 -rRNA -- 1.0625+Exit code: ExitSuccess+Satisfiable. Model:+  ENCODED = 1.125 :: UE5M3+                  76543 210+                  -E5-- S3-+   Binary layout: 01111 001+      Hex layout: 79+       Precision: 5 exponent bits, 3 significand bits+            Sign: Positive (always)+        Exponent: 0 (Stored: 15, Bias: 15)+  Classification: FP_NORMAL+          Binary: 0b1.001+           Octal: 0o1.1+         Decimal: 1.125+             Hex: 0x1.2+   Rounding mode: RNA: Round nearest ties to away.+            Note: Original value of 1.0625 was rounded to 1.125.
+ Golds/encodeUE5M3_tie_RNA_sub0.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RNA_sub1.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RNE_binade.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RNE_dev0.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RNE_dev1.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RNE_norm.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RNE_sub0.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RNE_sub1.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTN_binade.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTN_dev0.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTN_dev1.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTN_norm.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTN_sub0.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTN_sub1.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTP_binade.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTP_dev0.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTP_dev1.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTP_norm.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTP_sub0.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTP_sub1.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTZ_binade.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTZ_dev0.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTZ_dev1.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTZ_norm.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTZ_sub0.gold view

file too large to diff

+ Golds/encodeUE5M3_tie_RTZ_sub1.gold view

file too large to diff

+ Golds/encodeUE5M3_zero1.gold view

file too large to diff

+ Golds/encodeUE5M3_zero2.gold view

file too large to diff

crackNum.cabal view

file too large to diff

src/CrackNum/Encode.hs view

file too large to diff

src/CrackNum/TestSuite.hs view

file too large to diff

src/CrackNum/Utils.hs view

file too large to diff

+ test/TestMain.hs view

file too large to diff