failure in executing --- marlowe-cli run analyze

[albert-kevin]

$ marlowe-cli run analyze --testnet-magic 2 --marlowe-file tx-1.marlowe
marlowe-cli: Unable to locate executable for Z3
Executable specified: "z3"

CallStack (from HasCallStack):
error, called at ./Data/SBV/SMT/SMT.hs:648:23 in sbv-9.2-4eQ2GHybw8XBfYmavzuUka:Data.SBV.SMT.SMT

do you have any idea what I could try to find the issue here ?

[paluh]

Hi Kevin,

sorry for late response and thanks for the report:

• So AFAIK the analyzer requires z3 solver to be installed: https://github.com/Z3Prover/z3
• It is provided by Nix project env but if you are not using Nix it has to be probably installed separately.
• I will try to get more info but I'm not sure if I will be able to do any extra testing.
• I added an error report label because the message is not helpful and --help for this command doesn't provide any details about this requirement.

[albert-kevin]

hello paluh,
interesting thank you for your reply,
I am interested to install it separately.
I have a test system running where we could have a meeting together and walk through this and test together then share the insight here after.
I respect your time, let me know what you think

In the mean time I will try to figure out what I can...
ok, got the z3 installed, loading up cardano-node for a test...
it works now

Update package lists and install Z3

sudo sh -c 'apt update && apt install -y z3'

Verify Z3 installation

z3 -version

sync and load cardano-node

run the marlowe-cli run analyze command again