`avenir synth ...` command on hello example failing

[jafingerhut]

I have installed avenir on an Ubuntu 18.04 system using the script in this PR: #10

After installation, I have tried the avenir synth ... command recommended by Eric, which is now in the synthesis/README.md document verification section, but I am getting the error shown below. Any guesses whether this might be my installation script, or some other problem?

$ ../avenir synth abstract.p4 target.p4 inserts.csv no_edits.csv fvs -b 1000 -e 10 -data inserts.csv -I1 includes -I2 includes -P4 -p --hint mask --cache-edits 1 |& tee avenir-synth-1-out.txt
solver child (pid 2011), exited with return code 0, exited
solver child (pid 2014), exited with return code 0, exited
Uncaught exception:
  
  (Failure
   "expected model, got ((define-fun hdr.ipv4.srcAddr$1 () (_ BitVec 32) (_ bv0 32)) (define-fun phys_hdr.ipv4.srcAddr$0 () (_ BitVec 32) (_ bv0 32)) (define-fun phys_hdr.ethernet.srcAddr$0 () (_ BitVec 48) (_ bv281474976710655 48)) (define-fun ipv4_lpm_action_run$3 () (_ BitVec 2) (_ bv1 2)) (define-fun hdr.ethernet.dstAddr$0 () (_ BitVec 48) (_ bv0 48)) (define-fun hdr.ipv4.isValid$0 () (_ BitVec 1) (_ bv1 1)) (define-fun hdr.ipv4.ttl$1 () (_ BitVec 8) (_ bv0 8)) (define-fun hdr.ipv4.dstAddr$0 () (_ BitVec 32) (_ bv0 32)) (define-fun hdr.ipv4.isValid$1 () (_ BitVec 1) (_ bv1 1)) (define-fun hdr.ipv4.dstAddr$1 () (_ BitVec 32) (_ bv0 32)) (define-fun hdr.ethernet.srcAddr$1 () (_ BitVec 48) (_ bv0 48)) (define-fun standard_metadata.egress_spec$1 () (_ BitVec 9) (_ bv1 9)) (define-fun hdr.ipv4.ttl$2 () (_ BitVec 8) (_ bv0 8)) (define-fun hdr.ipv4.ttl$0 () (_ BitVec 8) (_ bv1 8)) (define-fun hdr.ethernet.srcAddr$2 () (_ BitVec 48) (_ bv0 48)) (define-fun hdr.ethernet.dstAddr$1 () (_ BitVec 48) (_ bv0 48)) (define-fun hdr.ethernet.dstAddr$2 () (_ BitVec 48) (_ bv0 48)) (define-fun phys_hdr.ipv4.srcAddr$1 () (_ BitVec 32) (_ bv0 32)) (define-fun phys_hdr.ipv4.dstAddr$1 () (_ BitVec 32) (_ bv0 32)) (define-fun phys_hdr.ipv4.ttl$1 () (_ BitVec 8) (_ bv0 8)) (define-fun phys_hdr.ethernet.dstAddr$1 () (_ BitVec 48) (_ bv0 48)) (define-fun phys_hdr.ethernet.srcAddr$1 () (_ BitVec 48) (_ bv0 48)) (define-fun phys_hdr.ipv4.isValid$1 () (_ BitVec 1) (_ bv0 1)) (define-fun phys_hdr.ipv4.isValid$0 () (_ BitVec 1) (_ bv1 1)) (define-fun phys_standard_metadata.egress_spec$2 () (_ BitVec 9) (_ bv0 9)) (define-fun phys_standard_metadata.egress_spec$1 () (_ BitVec 9) (_ bv0 9)) (define-fun ipv4_lpm_action_run$2 () (_ BitVec 2) (_ bv0 2)) (define-fun phys_ipv4_fwd_action_run$2 () (_ BitVec 2) (_ bv0 2)) (define-fun phys_ipv4_rewrite_action_run$2 () (_ BitVec 2) (_ bv0 2)) (define-fun phys_hdr.ipv4.ttl$0 () (_ BitVec 8) (_ bv1 8)) (define-fun hdr.ipv4.srcAddr$0 () (_ BitVec 32) (_ bv0 32)) (define-fun phys_hdr.ipv4.dstAddr$0 () (_ BitVec 32) (_ bv0 32)) (define-fun hdr.ethernet.srcAddr$0 () (_ BitVec 48) (_ bv281474976710655 48)) (define-fun phys_hdr.ethernet.dstAddr$0 () (_ BitVec 48) (_ bv0 48)) (define-fun phys_standard_metadata.egress_spec$3 () (_ BitVec 9) (_ bv0 9)) (define-fun phys_return3$2 () (_ BitVec 1) (_ bv0 1)) (define-fun phys_standard_metadata.egress_port$2 () (_ BitVec 9) (_ bv0 9)) (define-fun phys_standard_metadata.egress_spec$0 () (_ BitVec 9) (_ bv0 9)) (define-fun phys_standard_metadata.egress_port$1 () (_ BitVec 9) (_ bv0 9)) (define-fun phys_return4$1 () (_ BitVec 1) (_ bv0 1)) (define-fun phys_return3$1 () (_ BitVec 1) (_ bv0 1)) (define-fun phys_ipv4_rewrite_action_run$1 () (_ BitVec 2) (_ bv0 2)) (define-fun phys_ipv4_fwd_action_run$1 () (_ BitVec 2) (_ bv0 2)) (define-fun standard_metadata.egress_spec$2 () (_ BitVec 9) (_ bv1 9)) (define-fun return1$2 () (_ BitVec 1) (_ bv0 1)) (define-fun standard_metadata.egress_port$2 () (_ BitVec 9) (_ bv1 9)) (define-fun return2$2 () (_ BitVec 1) (_ bv0 1)) (define-fun standard_metadata.egress_spec$0 () (_ BitVec 9) (_ bv0 9)) (define-fun standard_metadata.egress_port$1 () (_ BitVec 9) (_ bv0 9)) (define-fun return2$1 () (_ BitVec 1) (_ bv0 1)) (define-fun return1$1 () (_ BitVec 1) (_ bv0 1)) (define-fun ipv4_lpm_action_run$1 () (_ BitVec 2) (_ bv0 2)) (define-fun phys_exit$1 () (_ BitVec 1) (_ bv0 1)) (define-fun phys_return4$2 () (_ BitVec 1) (_ bv0 1)))")

Raised at file "stdlib.ml", line 29, characters 17-33
Called from file "lib/Prover.ml", line 231, characters 8-37
Called from file "lib/Synthesis.ml", line 15, characters 7-35
Called from file "lib/Synthesis.ml", line 25, characters 8-49
Called from file "lib/Util.ml", line 242, characters 10-14
Called from file "lib/Synthesis.ml", line 248, characters 8-38
Called from file "list.ml", line 121, characters 24-34
Called from file "lib/Synthesis.ml", line 281, characters 19-63
Called from file "bin/Main.ml", line 256, characters 12-75
Called from file "src/command.ml", line 2453, characters 8-238
Called from file "src/exn.ml", line 111, characters 6-10

[ericthewry]

This is an issue with the Z3 interface. I vaguely remember coming across this before... I think the output changed version-to-version? What version do you have installed? I'm running 4.8.8.

[jafingerhut]

My install script installs version 4.8.10 right now. I can try having it install 4.8.8 instead, but the pre-built binaries have "ubuntu16.04" in their name, so I was a bit hesitant on using it on an Ubuntu 18.04 system on my first try. I will try changing the script to install z3 4.8.8 and see if that works.

[jnfoster]

You might find Z3's releases helpful here (rather than Ubuntu package managers).
https://github.com/Z3Prover/z3/releases/tag/z3-4.8.8
It also builds easily and quickly from source on most Linux distros.

[jafingerhut]

Thanks. I was aware of those, and the 4.8.8 version is exactly the one that has 'ubuntu16.04' in its name that I was shying away from initially. Again, I will try it out despite the fact it has 'ubuntu16.04' in its name, hoping it will also work on later ubuntu versions.

[ericthewry]

it runs for me on 20.04!

[jafingerhut]

Closing this, as I installed Z3 version 4.8.8 and now the command in the README is working. I have updated my PR with the install script to install that version of Z3.