Fix cli mistakes

[d-xo]

Description

Fixes two small mistakes in the cli interface:

1. We were ignoring the solver chosen by the user and always executing using Z3
2. The equivalence command had it's success condition backwards, and would report success for failure and vice versa...

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[msooseth]

isQed -> isCex otherwise great stuff :)

[asymmetric]

Any idea why this is failing on Linux and not on macOS?

[msooseth]

The PR pipeline tests broke (see logs here) because this randomly generation expression, unrated to the PR itself:

EVM.Expr.simplify WriteWord (SDiv (Sub (LT (Lit 0x1a) (Lit 0x2b)) (Lit 0x59)) (Lit 0x57)) (Lit 0xba0f7483eaf0000033e5f50af97000007b670a8fe8e000017b866ff8ee9) (WriteWord (Lit 0x10) (Lit 0x194f1c1b0a5600000ccdec88b707000004743426102c000005e06b915fdc) (AbstractBuf "esc_NFIIGOFlwfrBCZWnIWOEvFBT"))

Overflows Expr.simplify, in particular, the offset (SDiv (Sub (LT (Lit 0x1a) (Lit 0x2b)) (Lit 0x59)) (Lit 0x57)) happens to be:

EVM.Expr.simplify (SDiv (Sub (LT (Lit 0x1a) (Lit 0x2b)) (Lit 0x59)) (Lit 0x57))
Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff

i.e. very large. This is related to the CopySlice simplifier overflow, where a similar issue happened and has been fixed by @zoep .

[msooseth]

I am re-running the PR pipeline, and created the issue #207 to track the problem itself so we can merge this unrelated fix and fix the other issue separately.