Z3 model parsing bug

[edenfrenkel]

Program panics when executing
echo -e "3\nE quorum q\nF node n1 n2 n3\nF value v\n0\n3" | cargo run --release -- infer examples/consensus_epr.fly --solver z3

Error message: thread 'main' panicked at 'could not find relation k!1058', src/fly/syntax.rs:218:32

Running with RUST_BACKTRACE=1 yields the following trace

   0: rust_begin_unwind
             at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:584:5`
   1: core::panicking::panic_fmt
             at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/core/src/panicking.rs:142:14`
   2: temporal_verifier::fly::syntax::Signature::relation_decl`
   3: <&temporal_verifier::solver::backends::GenericBackend as temporal_verifier::solver::imp::Backend>::parse
   4: temporal_verifier::solver::imp::Solver<B>::get_fo_model
   5: temporal_verifier::solver::imp::Solver<B>::get_minimal_model
   6: temporal_verifier::inference::basics::FOModule::trans_cex
   7: temporal_verifier::inference::basics::Frame<T>::get_cex_trans
   8: temporal_verifier::inference::fixpoint::run_fixpoint
   9: temporal_verifier::command::App::exec
  10: temporal_verifier::main

[tchajed]

Thanks for the report! I fixed this in the branch fix-issue-5. This example now runs with z3, although it's very slow.

We can merge that once the inference branch is ready to go. (Technically it doesn't rely on anything from that branch, but this example is the only test exercising the new behavior for now.)