SAW's simulator doesn't short-circuit evaluation like Cryptol does

[RyanGlScott]

Consider the following Cryptol property:

\b -> b ==> (b \/ error "uh oh") }}

Cryptol's evaluation order allows proving this property without ever triggering the error:

Cryptol> :prove \b -> b ==> (b \/ error "uh oh")
Q.E.D.
(Total Elapsed Time: 0.021s, using "Z3")

SAW's simulator, on the other hand, will not short-circuit during evaluation, and as a result, it will trigger this error:

sawscript> prove_print z3 {{ \b -> b ==> (b \/ error "uh oh") }};

Run-time error: encountered call to the Cryptol 'error' function

This is something that I originally discovered while investigating #1807. While the example above is somewhat contrived, my proposed fix for #1807 would cause SAW to eagerly evaluate errors in more places, such as in the following property:

\(x : [2]) (i : [2]) -> (i < 2) ==> (x @ i) >= 42

Note that array indexing (@) calls error under the hood when the index value exceeds the length of the array. Due to #1807, SAW's simulator will effectively "clamp" the index value to be less than the length of the array, which means that SAW's simulator never even considers the cases where i = 2 or i = 3. But if I implement my proposed fix, then SAW does consider these cases, and due the aforementioned differences in short-circuiting behavior between Cryptol and SAW, adding (i < 2) ==> ... isn't enough to avoid out-of-bounds indexes.

To put it more directly: this issue is a blocker for fixing #1807.

[RyanGlScott]

Cryptol is very careful not to invoke errors on one side of a symbolic merge when the condition being merged on allows short-circuiting (see this code). One possible approach to fixing this issue is to implement something similar in saw-core's muxValue function. Unfortunately, this wouldn't be quite as straightforward as in Cryptol, as calls to error in SAWCore become raw Haskell exceptions.

[sauclovian-g]

This is related to #2124 but the latter is more general and seems to involve failure to track path conditions correctly.