Test problematic SMT formulas from Cryptol's `negshift` test case

[RyanGlScott]

Cryptol's negshift test suite is particularly troublesome, as the SMT formulas that it generates have been known to cause certain version of Z3 to nondeterministically go into an infinite loop. See GaloisInc/cryptol#1107. It would be worth minimizing the SMT-LIB from this test case into something that could be checked into what4's own test suite, as what4's CI tests a broad matrix of SMT solver versions. This could give us some additional insight into which versions of solvers we should actually use in upstream projects' CI.