Provide counterexamples in hexadecimal

[bboston7]

A few SAW learners have mentioned to me that they would find SAW counterexamples to be more useful if they were in hexadecimal, or if there were an option like :set base in Cryptol to change the default for counterexamples from decimal to hexadecimal.

One example:

[00:12:49.938] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 550}
[00:12:49.938] ----------Counterexample----------
[00:12:49.938]   x: 205214799977500604566419154610474108846
[00:12:49.938] ----------------------------------
[00:12:49.938] Stack trace:
"llvm_verify" (/workspaces/exercises/functional-correctness/u128/exercise.saw:27:1-27:12):
Proof failed.

[weaversa]

This is an easy one!

sawscript> :h set_base
Description
-----------

    set_base : Int -> TopLevel ()

Set the number base for pretty-printing numeric literals.
Permissible values include 2, 8, 10, and 16.
sawscript> set_base 16
sawscript> sat z3 {{ \(x : [32]) -> x + 100 > x }}
[01:41:57.468] Sat: [x = 0x3f8c]
sawscript> sat z3 {{ \(x : [32]) -> x + 100 < x }}
[01:42:00.324] Sat: [x = 0xffffffbc]

[bboston7]

Huh, I'm surprised I didn't know about that one! I'll close this issue then. Thanks @weaversa!

[weaversa]

Well, it could be improved...you'll notice in the counterexamples gotten in my example, the first one 0x3f8c won't type check in Cryptol because the output is supposed to be of type [32]. It would be nicer if the counterexample was printed as `0x00003f8c'.