Tweak satisfiability check of the remainder branch

[geo2a]

This PR makes sure the remainder predicate is checked considering the available side condition.

[geo2a]

EDIT: was running with 5 workers, it seems we have severe noise issues again...

Hmm, the performance of KEVM actually seems worse:

| Test                                                  | georgy-check-remainder-consider-side-condition time | master-974ab83b0 time | (georgy-check-remainder-consider-side-condition/master-974ab83b0) time
|-------------------------------------------------------|-----------------------------------------------------|-----------------------|------------------------------------------------------------------------
| erc20/ds/allowance-spec.k                             | 42.13                                               | 48.89                 | 0.861730415217836
| functional/storageRoot-spec.k                         | 155.34                                              | 161.75                | 0.9603709428129831
| benchmarks/overflow00-overflow-spec.k                 | 45.34                                               | 47.19                 | 0.9607967789785973
| benchmarks/keccak00-spec.k                            | 48.75                                               | 46.47                 | 1.0490639122014203
| mcd/flopper-file-pass-rough-spec.k                    | 446.22                                              | 423.79                | 1.0529271573184833
| kontrol/test-storetest-testaccesses-0-spec.k          | 78.01                                               | 71.13                 | 1.0967243076057924
| mcd/flopper-kick-pass-rough-spec.k                    | 139.65                                              | 123.35                | 1.1321443048236726
| benchmarks/ecrecoverloop02-sigs-valid-spec.k          | 596.73                                              | 494.15                | 1.2075887888293029
| erc20/ds/transferFrom-failure-1-a-spec.k              | 89.42                                               | 69.59                 | 1.2849547348757004
| mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k | 1332.64                                             | 1026.67               | 1.2980217596696115
| examples/solidity-code-spec.md                        | 177.8                                               | 136.79                | 1.2998026171503767
| mcd/flipper-ttl-pass-spec.k                           | 97.15                                               | 70.57                 | 1.376647300552643
| erc20/ds/balanceOf-spec.k                             | 64.58                                               | 44.8                  | 1.4415178571428573
| benchmarks/functional-spec.k                          | 583.17                                              | 399.38                | 1.460188291852371
| erc20/ds/approve-success-spec.k                       | 90.62                                               | 58.45                 | 1.5503849443969204
| erc20/ds/transfer-success-2-spec.k                    | 92.36                                               | 59.25                 | 1.558818565400844
| erc20/ds/approve-failure-spec.k                       | 70.77                                               | 45.13                 | 1.5681364945712384
| erc20/ds/transfer-success-1-spec.k                    | 99.16                                               | 62.52                 | 1.586052463211772
| benchmarks/staticloop00-a0lt10-spec.k                 | 91.28                                               | 52.7                  | 1.7320683111954458
| erc20/ds/transfer-failure-1-b-spec.k                  | 153.88                                              | 88.58                 | 1.7371867238654324
| erc20/ds/transfer-failure-1-a-spec.k                  | 119.67                                              | 68.44                 | 1.7485388661601404
| kontrol/test-storetest-teststoreload-0-spec.k         | 88.62                                               | 49.61                 | 1.786333400524088
| erc20/ds/transfer-failure-2-a-spec.k                  | 121.03                                              | 67.52                 | 1.7925059241706163
| benchmarks/encodepacked-keccak01-spec.k               | 86.15                                               | 47.81                 | 1.8019242836226732
| benchmarks/requires01-a0le0-spec.k                    | 84.57                                               | 46.88                 | 1.8039675767918086
| benchmarks/requires01-a0gt0-spec.k                    | 85.1                                                | 46.86                 | 1.8160478019632948
| erc20/ds/transfer-failure-1-c-spec.k                  | 88.14                                               | 48.45                 | 1.8191950464396285
| benchmarks/storagevar02-nooverflow-spec.k             | 84.06                                               | 46.07                 | 1.8246147167354028
| benchmarks/storagevar00-spec.k                        | 85.09                                               | 46.49                 | 1.8302860830286083
| mcd/flopper-cage-pass-spec.k                          | 101.1                                               | 55.19                 | 1.8318535966660627
| benchmarks/encode-keccak00-spec.k                     | 90.86                                               | 49.45                 | 1.837411526794742
| benchmarks/staticarray00-spec.k                       | 85.16                                               | 46.21                 | 1.842891149101926
| erc20/ds/transfer-failure-2-b-spec.k                  | 87.27                                               | 47.29                 | 1.8454218650877563
| benchmarks/storagevar01-spec.k                        | 82.88                                               | 44.5                  | 1.8624719101123595
| functional/lemmas-spec.k                              | 1008.01                                             | 91.02                 | 11.074598989233136
| TOTAL                                                 | 6792.710000000002                                   | 4332.9400000000005    | 1.5676907596227967

note that functional/lemmas-spec.k actually failed on master, which seems suspicious.

[geo2a]

A KEVM performance run with 1 worker isn't showing any difference:

| Test                                           | georgy-check-remainder-consider-side-condition time | master-974ab83b0 time | (georgy-check-remainder-consider-side-condition/master-974ab83b0) time
|------------------------------------------------|-----------------------------------------------------|-----------------------|------------------------------------------------------------------------
| benchmarks/ecrecoverloop02-sig0-invalid-spec.k | 210.77                                              | 221.67                | 0.9508278071006452
| mcd/dsvalue-peek-pass-rough-spec.k             | 50.85                                               | 48.99                 | 1.0379669320269442
| mcd/flopper-tick-pass-rough-spec.k             | 234.06                                              | 223.94                | 1.0451906760739484
| mcd/dstoken-approve-fail-rough-spec.k          | 89.51                                               | 85.45                 | 1.0475131655939145
| benchmarks/ecrecoverloop02-sigs-valid-spec.k   | 431.36                                              | 407.54                | 1.0584482504784807
| TOTAL                                          | 1016.5500000000001                                  | 987.5899999999999     | 1.0293239097196207

[geo2a]

Closing this for now, as it does not bring any benefit, and we are likely to tweak this behavior in a slightly different way in other PRs.