ASM Equivalence Checker: Use bounds from the dag

<details><summary>Timing Diff</summary>
<p>

```
     After |   Peak Mem | File Name                                                 |     Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------------------------------------------
158m20.95s | 4393964 ko | Total Time / Peak Mem                                     | 156m15.65s | 4393936 ko || +2m05.29s ||        28 ko |   +1.33% |         +0.00%
----------------------------------------------------------------------------------------------------------------------------------------------------------------------
 41m01.08s |  381660 ko | fiat-amd64/p434-square.status                             |  39m28.73s |  392032 ko || +1m32.34s ||    -10372 ko |   +3.89% |         -2.64%
  4m32.02s |  106160 ko | fiat-amd64/p384-square.status                             |   4m13.46s |  107844 ko || +0m18.55s ||     -1684 ko |   +7.32% |         -1.56%
  5m01.88s |  112276 ko | fiat-amd64/p384-mul.status                                |   4m59.41s |  117724 ko || +0m02.47s ||     -5448 ko |   +0.82% |         -4.62%
  1m49.45s | 2241388 ko | Fancy/Barrett256.vo                                       |   1m51.54s | 2241304 ko || -0m02.08s ||        84 ko |   -1.87% |         +0.00%
  1m02.93s | 4393964 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo                  |   1m00.82s | 4393936 ko || +0m02.10s ||        28 ko |   +3.46% |         +0.00%
  0m32.74s |   55196 ko | fiat-amd64/p448-square.status                             |   0m35.35s |   54524 ko || -0m02.60s ||       672 ko |   -7.38% |         +1.23%
  0m21.12s |   43776 ko | fiat-amd64/secp256k1-mul.status                           |   0m18.18s |   44332 ko || +0m02.94s ||      -556 ko |  +16.17% |         -1.25%
  1m34.95s |   71336 ko | fiat-amd64/p448-mul.status                                |   1m36.14s |   71528 ko || -0m01.18s ||      -192 ko |   -1.23% |         -0.26%
  0m43.46s | 2148100 ko | ExtractionOCaml/bedrock2_solinas_reduction                |   0m41.91s | 2148060 ko || +0m01.55s ||        40 ko |   +3.69% |         +0.00%
  0m31.75s | 1520824 ko | StandaloneDebuggingExamples.vo                            |   0m30.17s | 1520896 ko || +0m01.57s ||       -72 ko |   +5.23% |         -0.00%
  0m20.87s | 1874548 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml           |   0m19.73s | 1874660 ko || +0m01.14s ||      -112 ko |   +5.77% |         -0.00%
  0m19.03s |   45236 ko | fiat-amd64/secp256k1-square.status                        |   0m17.21s |   44724 ko || +0m01.82s ||       512 ko |  +10.57% |         +1.14%
  0m14.65s |   44880 ko | fiat-amd64/p521-square.status                             |   0m13.42s |   45636 ko || +0m01.23s ||      -756 ko |   +9.16% |         -1.65%
 47m04.34s |  403740 ko | fiat-amd64/p434-mul.status                                |  47m03.56s |  415872 ko || +0m00.78s ||    -12132 ko |   +0.02% |         -2.91%
 10m09.41s | 2592812 ko | Bedrock/End2End/X25519/GarageDoor.vo                      |  10m10.08s | 2592672 ko || -0m00.67s ||       140 ko |   -0.10% |         +0.00%
  5m34.52s | 2784892 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo           |   5m34.14s | 2784788 ko || +0m00.37s ||       104 ko |   +0.11% |         +0.00%
  4m12.67s | 2567008 ko | Assembly/WithBedrock/Proofs.vo                            |   4m11.98s | 2566796 ko || +0m00.68s ||       212 ko |   +0.27% |         +0.00%
  1m53.50s | 1596296 ko | Bedrock/End2End/X25519/Field25519.vo                      |   1m53.69s | 1595988 ko || -0m00.18s ||       308 ko |   -0.16% |         +0.01%
  1m39.23s | 1511380 ko | Assembly/EquivalenceProofs.vo                             |   1m39.70s | 1511392 ko || -0m00.47s ||       -12 ko |   -0.47% |         -0.00%
  1m29.49s | 2008892 ko | SlowPrimeSynthesisExamples.vo                             |   1m29.42s | 2008852 ko || +0m00.06s ||        40 ko |   +0.07% |         +0.00%
  1m12.44s | 1428436 ko | Assembly/WithBedrock/SymbolicProofs.vo                    |   1m12.17s | 1428424 ko || +0m00.26s ||        12 ko |   +0.37% |         +0.00%
  1m02.94s |   64012 ko | fiat-amd64/p521-mul.status                                |   1m02.87s |   64192 ko || +0m00.07s ||      -180 ko |   +0.11% |         -0.28%
  0m47.62s | 1746252 ko | Fancy/Montgomery256.vo                                    |   0m47.45s | 1746172 ko || +0m00.16s ||        80 ko |   +0.35% |         +0.00%
  0m46.31s | 1483736 ko | Assembly/Symbolic.vo                                      |   0m46.11s | 1482844 ko || +0m00.20s ||       892 ko |   +0.43% |         +0.06%
  0m42.42s | 2147892 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery     |   0m42.25s | 2147924 ko || +0m00.17s ||       -32 ko |   +0.40% |         -0.00%
  0m41.62s | 2147952 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery          |   0m41.65s | 2147836 ko || -0m00.03s ||       116 ko |   -0.07% |         +0.00%
  0m41.10s | 2147880 ko | ExtractionOCaml/solinas_reduction                         |   0m41.07s | 2147912 ko || +0m00.03s ||       -32 ko |   +0.07% |         -0.00%
  0m40.53s | 1779308 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas         |   0m40.66s | 1780496 ko || -0m00.12s ||     -1188 ko |   -0.31% |         -0.06%
  0m40.12s | 1779684 ko | ExtractionOCaml/bedrock2_unsaturated_solinas              |   0m39.13s | 1779368 ko || +0m00.98s ||       316 ko |   +2.53% |         +0.01%
  0m39.97s | 2147984 ko | ExtractionOCaml/word_by_word_montgomery                   |   0m40.17s | 2147956 ko || -0m00.20s ||        28 ko |   -0.49% |         +0.00%
  0m38.47s | 1286368 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo                |   0m38.09s | 1286304 ko || +0m00.37s ||        64 ko |   +0.99% |         +0.00%
  0m38.35s | 1689328 ko | ExtractionOCaml/unsaturated_solinas                       |   0m38.34s | 1688416 ko || +0m00.00s ||       912 ko |   +0.02% |         +0.05%
  0m37.50s | 1453656 ko | ExtractionOCaml/with_bedrock2_solinas_reduction           |   0m37.25s | 1453924 ko || +0m00.25s ||      -268 ko |   +0.67% |         -0.01%
  0m37.28s | 1453524 ko | ExtractionOCaml/with_bedrock2_saturated_solinas           |   0m37.55s | 1453772 ko || -0m00.26s ||      -248 ko |   -0.71% |         -0.01%
  0m37.18s | 1442572 ko | ExtractionOCaml/bedrock2_saturated_solinas                |   0m37.21s | 1457092 ko || -0m00.03s ||    -14520 ko |   -0.08% |         -0.99%
  0m36.66s | 1450972 ko | ExtractionOCaml/with_bedrock2_base_conversion             |   0m36.41s | 1455392 ko || +0m00.25s ||     -4420 ko |   +0.68% |         -0.30%
  0m36.05s | 1446756 ko | ExtractionOCaml/bedrock2_base_conversion                  |   0m36.44s | 1453460 ko || -0m00.39s ||     -6704 ko |   -1.07% |         -0.46%
  0m35.39s | 2285364 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml             |   0m34.77s | 2285512 ko || +0m00.61s ||      -148 ko |   +1.78% |         -0.00%
  0m34.64s | 2242900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml  |   0m33.78s | 2243116 ko || +0m00.85s ||      -216 ko |   +2.54% |         -0.00%
  0m34.51s | 2243024 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml       |   0m34.38s | 2242944 ko || +0m00.12s ||        80 ko |   +0.37% |         +0.00%
  0m34.26s | 1415884 ko | ExtractionOCaml/saturated_solinas                         |   0m34.59s | 1415904 ko || -0m00.33s ||       -20 ko |   -0.95% |         -0.00%
  0m34.19s | 2168928 ko | ExtractionOCaml/solinas_reduction.ml                      |   0m33.30s | 2168964 ko || +0m00.89s ||       -36 ko |   +2.67% |         -0.00%
  0m33.90s | 1415988 ko | ExtractionOCaml/base_conversion                           |   0m33.80s | 1415884 ko || +0m00.10s ||       104 ko |   +0.29% |         +0.00%
  0m33.21s | 2132400 ko | ExtractionOCaml/word_by_word_montgomery.ml                |   0m33.29s | 2132328 ko || -0m00.07s ||        72 ko |   -0.24% |         +0.00%
  0m31.51s | 2164380 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml      |   0m31.35s | 2164248 ko || +0m00.16s ||       132 ko |   +0.51% |         +0.00%
  0m30.99s | 2164352 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml           |   0m31.90s | 2164568 ko || -0m00.91s ||      -216 ko |   -2.85% |         -0.00%
  0m29.84s | 2043944 ko | ExtractionOCaml/unsaturated_solinas.ml                    |   0m29.78s | 2043888 ko || +0m00.05s ||        56 ko |   +0.20% |         +0.00%
  0m29.40s | 1232240 ko | ExtractionOCaml/perf_word_by_word_montgomery              |   0m28.54s | 1232264 ko || +0m00.85s ||       -24 ko |   +3.01% |         -0.00%
  0m28.97s | 1232260 ko | ExtractionOCaml/perf_unsaturated_solinas                  |   0m28.70s | 1232424 ko || +0m00.26s ||      -164 ko |   +0.94% |         -0.01%
  0m27.51s | 2053200 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml             |   0m27.43s | 2053140 ko || +0m00.08s ||        60 ko |   +0.29% |         +0.00%
  0m27.34s | 2036072 ko | ExtractionOCaml/bedrock2_base_conversion.ml               |   0m27.47s | 2035968 ko || -0m00.12s ||       104 ko |   -0.47% |         +0.00%
  0m27.34s | 2052988 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml        |   0m27.21s | 2053060 ko || +0m00.12s ||       -72 ko |   +0.47% |         -0.00%
  0m27.30s | 2053260 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml        |   0m27.45s | 2053064 ko || -0m00.14s ||       196 ko |   -0.54% |         +0.00%
  0m26.56s | 2036256 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml          |   0m27.33s | 2036248 ko || -0m00.76s ||         8 ko |   -2.81% |         +0.00%
  0m26.00s | 1988816 ko | ExtractionOCaml/base_conversion.ml                        |   0m25.32s | 1988820 ko || +0m00.67s ||        -4 ko |   +2.68% |         -0.00%
  0m25.75s | 1956940 ko | ExtractionOCaml/saturated_solinas.ml                      |   0m25.70s | 1956860 ko || +0m00.05s ||        80 ko |   +0.19% |         +0.00%
  0m25.19s | 1166872 ko | PushButtonSynthesis/UnsaturatedSolinas.vo                 |   0m25.03s | 1166932 ko || +0m00.16s ||       -60 ko |   +0.63% |         -0.00%
  0m23.77s | 1375040 ko | Bedrock/End2End/RupicolaCrypto/Low.vo                     |   0m23.78s | 1375196 ko || -0m00.01s ||      -156 ko |   -0.04% |         -0.01%
  0m22.42s | 1138632 ko | PushButtonSynthesis/WordByWordMontgomery.vo               |   0m22.39s | 1138516 ko || +0m00.03s ||       116 ko |   +0.13% |         +0.01%
  0m19.45s | 1820840 ko | ExtractionOCaml/perf_unsaturated_solinas.ml               |   0m19.96s | 1820960 ko || -0m00.51s ||      -120 ko |   -2.55% |         -0.00%
  0m19.39s | 1152200 ko | Bedrock/Field/Translation/Proofs/Cmd.vo                   |   0m19.27s | 1152320 ko || +0m00.12s ||      -120 ko |   +0.62% |         -0.01%
  0m19.10s | 1121332 ko | Bedrock/Field/Translation/Proofs/Func.vo                  |   0m19.14s | 1121364 ko || -0m00.03s ||       -32 ko |   -0.20% |         -0.00%
  0m19.07s |   46832 ko | fiat-amd64/p224-mul.status                                |   0m19.32s |   46944 ko || -0m00.25s ||      -112 ko |   -1.29% |         -0.23%
  0m18.34s | 1196504 ko | Bedrock/Field/Synthesis/New/Signature.vo                  |   0m18.22s | 1196540 ko || +0m00.12s ||       -36 ko |   +0.65% |         -0.00%
  0m18.10s |   46980 ko | fiat-amd64/p224-square.status                             |   0m17.17s |   45956 ko || +0m00.92s ||      1024 ko |   +5.41% |         +2.22%
  0m17.85s | 1119980 ko | Bedrock/End2End/Poly1305/Field1305.vo                     |   0m17.94s | 1119912 ko || -0m00.08s ||        68 ko |   -0.50% |         +0.00%
  0m13.11s | 1027008 ko | BoundsPipeline.vo                                         |   0m13.31s | 1027120 ko || -0m00.20s ||      -112 ko |   -1.50% |         -0.01%
  0m11.77s | 1718472 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo       |   0m11.91s | 1718332 ko || -0m00.14s ||       140 ko |   -1.17% |         +0.00%
  0m10.95s | 1317672 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo      |   0m10.84s | 1317672 ko || +0m00.10s ||         0 ko |   +1.01% |         +0.00%
  0m09.81s | 1025496 ko | PushButtonSynthesis/BaseConversion.vo                     |   0m09.82s | 1025432 ko || -0m00.00s ||        64 ko |   -0.10% |         +0.00%
  0m09.01s |   40320 ko | fiat-amd64/p256-square.status                             |   0m08.73s |   38692 ko || +0m00.27s ||      1628 ko |   +3.20% |         +4.20%
  0m08.94s | 1036420 ko | PushButtonSynthesis/Primitives.vo                         |   0m08.86s | 1036424 ko || +0m00.08s ||        -4 ko |   +0.90% |         -0.00%
  0m08.75s |  996628 ko | PushButtonSynthesis/SmallExamples.vo                      |   0m08.76s |  996492 ko || -0m00.00s ||       136 ko |   -0.11% |         +0.01%
  0m07.62s | 1028808 ko | PushButtonSynthesis/SolinasReduction.vo                   |   0m07.65s | 1028920 ko || -0m00.03s ||      -112 ko |   -0.39% |         -0.01%
  0m06.58s | 1036084 ko | PushButtonSynthesis/BarrettReduction.vo                   |   0m06.56s | 1035952 ko || +0m00.02s ||       132 ko |   +0.30% |         +0.01%
  0m06.29s | 1084688 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo         |   0m06.24s | 1084704 ko || +0m00.04s ||       -16 ko |   +0.80% |         -0.00%
  0m06.15s | 1115844 ko | CLI.vo                                                    |   0m06.21s | 1116052 ko || -0m00.05s ||      -208 ko |   -0.96% |         -0.01%
  0m04.83s | 1058816 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo   |   0m04.85s | 1058816 ko || -0m00.01s ||         0 ko |   -0.41% |         +0.00%
  0m04.59s | 1030100 ko | PushButtonSynthesis/SaturatedSolinas.vo                   |   0m04.63s | 1029984 ko || -0m00.04s ||       116 ko |   -0.86% |         +0.01%
  0m03.96s | 1039660 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo           |   0m04.07s | 1039672 ko || -0m00.11s ||       -12 ko |   -2.70% |         -0.00%
  0m03.62s |  949392 ko | Assembly/Equivalence.vo                                   |   0m03.69s |  949320 ko || -0m00.06s ||        72 ko |   -1.89% |         +0.00%
  0m03.25s | 1004124 ko | Bedrock/Field/Translation/Cmd.vo                          |   0m03.32s | 1004056 ko || -0m00.06s ||        68 ko |   -2.10% |         +0.00%
  0m03.19s | 1001624 ko | Bedrock/Field/Translation/Func.vo                         |   0m03.07s | 1001804 ko || +0m00.12s ||      -180 ko |   +3.90% |         -0.01%
  0m03.17s | 1071332 ko | Rewriter/PerfTesting/Core.vo                              |   0m03.18s | 1071324 ko || -0m00.01s ||         8 ko |   -0.31% |         +0.00%
  0m02.94s | 1112208 ko | StandaloneHaskellMain.vo                                  |   0m02.87s | 1112204 ko || +0m00.06s ||         4 ko |   +2.43% |         +0.00%
  0m02.93s | 1138092 ko | Bedrock/Standalone/StandaloneHaskellMain.vo               |   0m02.92s | 1138104 ko || +0m00.01s ||       -12 ko |   +0.34% |         -0.00%
  0m02.92s | 1050604 ko | Bedrock/Field/Stringification/Stringification.vo          |   0m02.96s | 1050496 ko || -0m00.04s ||       108 ko |   -1.35% |         +0.01%
  0m02.90s | 1112868 ko | StandaloneOCamlMain.vo                                    |   0m02.90s | 1112708 ko || +0m00.00s ||       160 ko |   +0.00% |         +0.01%
  0m02.88s | 1119908 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo               |   0m02.64s | 1120020 ko || +0m00.23s ||      -112 ko |   +9.09% |         -0.00%
  0m02.84s | 1055540 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo  |   0m02.81s | 1055568 ko || +0m00.02s ||       -28 ko |   +1.06% |         -0.00%
  0m02.82s | 1138076 ko | Bedrock/Standalone/StandaloneOCamlMain.vo                 |   0m02.71s | 1138148 ko || +0m00.10s ||       -72 ko |   +4.05% |         -0.00%
  0m02.81s |   30932 ko | fiat-amd64/curve25519-mul.status                          |   0m02.76s |   30944 ko || +0m00.05s ||       -12 ko |   +1.81% |         -0.03%
  0m02.73s | 1062448 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo                 |   0m02.89s | 1062560 ko || -0m00.16s ||      -112 ko |   -5.53% |         -0.01%
  0m02.64s | 1042004 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo        |   0m02.61s | 1041752 ko || +0m00.03s ||       252 ko |   +1.14% |         +0.02%
  0m02.61s | 1037976 ko | Bedrock/Field/Translation/Parameters/Defaults.vo          |   0m02.60s | 1038084 ko || +0m00.00s ||      -108 ko |   +0.38% |         -0.01%
  0m02.61s | 1041780 ko | Bedrock/Field/Translation/Parameters/FE310.vo             |   0m02.61s | 1041952 ko || +0m00.00s ||      -172 ko |   +0.00% |         -0.01%
  0m02.59s | 1041976 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo        |   0m02.71s | 1042004 ko || -0m00.12s ||       -28 ko |   -4.42% |         -0.00%
  0m02.00s |   29380 ko | fiat-amd64/curve25519-square.status                       |   0m01.94s |   29828 ko || +0m00.06s ||      -448 ko |   +3.09% |         -1.50%
  0m00.92s |   25544 ko | fiat-amd64/poly1305-mul.status                            |   0m00.92s |   25720 ko || +0m00.00s ||      -176 ko |   +0.00% |         -0.68%
  0m00.81s |   25704 ko | fiat-amd64/poly1305-square.status                         |   0m00.79s |   25496 ko || +0m00.02s ||       208 ko |   +2.53% |         +0.81%
  0m00.58s |  119548 ko | ExtractionOCaml/base_conversion.cmi                       |   0m00.51s |  119480 ko || +0m00.06s ||        68 ko |  +13.72% |         +0.05%
  0m00.57s |  120004 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi          |   0m00.57s |  120036 ko || +0m00.00s ||       -32 ko |   +0.00% |         -0.02%
  0m00.57s |  123072 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi      |   0m00.57s |  123096 ko || +0m00.00s ||       -24 ko |   +0.00% |         -0.01%
  0m00.56s |  123140 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi |   0m00.52s |  123084 ko || +0m00.04s ||        56 ko |   +7.69% |         +0.04%
  0m00.55s |  122368 ko | ExtractionOCaml/bedrock2_base_conversion.cmi              |   0m00.55s |  122304 ko || +0m00.00s ||        64 ko |   +0.00% |         +0.05%
  0m00.54s |  122252 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi         |   0m00.54s |  122292 ko || +0m00.00s ||       -40 ko |   +0.00% |         -0.03%
  0m00.54s |  122424 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi       |   0m00.51s |  122648 ko || +0m00.03s ||      -224 ko |   +5.88% |         -0.18%
  0m00.54s |  119968 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi     |   0m00.54s |  120168 ko || +0m00.00s ||      -200 ko |   +0.00% |         -0.16%
  0m00.54s |  121308 ko | ExtractionOCaml/word_by_word_montgomery.cmi               |   0m00.56s |  121284 ko || -0m00.02s ||        24 ko |   -3.57% |         +0.01%
  0m00.53s |  122188 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi            |   0m00.55s |  122312 ko || -0m00.02s ||      -124 ko |   -3.63% |         -0.10%
  0m00.52s |  122696 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi            |   0m00.53s |  122364 ko || -0m00.01s ||       332 ko |   -1.88% |         +0.27%
  0m00.52s |  122568 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi       |   0m00.54s |  122660 ko || -0m00.02s ||       -92 ko |   -3.70% |         -0.07%
  0m00.51s |  120012 ko | ExtractionOCaml/solinas_reduction.cmi                     |   0m00.55s |  120128 ko || -0m00.04s ||      -116 ko |   -7.27% |         -0.09%
  0m00.51s |  121160 ko | ExtractionOCaml/unsaturated_solinas.cmi                   |   0m00.54s |  121324 ko || -0m00.03s ||      -164 ko |   -5.55% |         -0.13%
  0m00.50s |  120828 ko | ExtractionOCaml/saturated_solinas.cmi                     |   0m00.55s |  120584 ko || -0m00.05s ||       244 ko |   -9.09% |         +0.20%
  0m00.18s |   61076 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi          |   0m00.18s |   61168 ko || +0m00.00s ||       -92 ko |   +0.00% |         -0.15%
  0m00.16s |   61240 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi              |   0m00.19s |   61160 ko || -0m00.03s ||        80 ko |  -15.78% |         +0.13%
  0m00.06s |   20944 ko | fiat-amd64/p224-sub.status                                |   0m00.05s |   21032 ko || +0m00.00s ||       -88 ko |  +19.99% |         -0.41%

```
</p>
</details>

src/Assembly/Symbolic.v

@@ -2231,7 +2231,7 @@ Section bound_expr_via_PHOAS.
               => o (List.map (fun e 'tt => bound_expr_via_PHOAS d e) args)
             | None => None
             end
-       | ExprRef _ => None
+       | ExprRef i => dag.lookup_bounds d i
        end.
 
   Local Coercion is_true : bool >-> Sortclass.