Use z3str3 string solver.
Use z3str3 string solver.

This solver produces better strings, in two ways:

1. It produces nicer strings in general (examples via
https://github.com/Z3Prover/z3/issues/1614):

z3str3:

(model
  (define-fun s2 () String
    "aaaC\x00")
  (define-fun s1 () String
    "aaaaaaa2")
)

default (seq solver):

(model
  (define-fun s2 () String
    "\x04\x10\x04\x10\x00")
  (define-fun s1 () String
    "\x00\x00\x00\x00\x00\x00\x00\x00")
)

2. It doesn't seem to reuse strings that make no sense in context.

z3str3:

    Warning: Invalidating model found:
      Program trace:
        entering pact test.payment with arguments
          payer = "aaaC"
          payer-entity = "aae"
          payee = "aF"
          payee-entity = "aad"
          amount = -1
          payer-bal = 0
          payee-bal = 1
      ...

default:

    Warning: Invalidating model found:
      Program trace:
        entering pact test.payment with arguments
          payer = "step 1"
          payer-entity = ""
          payee = "INTERNAL: pact done"
          payee-entity = ""
          amount = 1
          payer-bal = 2
          payee-bal = 0
      ...

Note how payer / payee reuse strings found elsewhere in the constraint
set, that are confusing in this context.

kadena-io/pact,kadena-io/pact,kadena-io/pact,kadena-io/pact