Working example rubixi - panic exeption

[mstad]

I installed in ubuntu 18.04 ethBMC with:

• rustc 1.52.0-nightly (caca2121f 2021-03-05)
• geth 1.8.27-stable-4bcc0a37
• Yices 2.6.2

After launching the' cargo build --release' in the main EthBMC folder,
I receive some following warnings:
------------------- 1 -------------------------
Compiling ethereum-newtypes v0.1.0 (/home/mirkostad/Programmi/EthBMC-master/evmexec/ethereum-newtypes)
warning: unused doc comment
--> evmexec/ethereum-newtypes/src/lib.rs:16:1
|
16 | /// A wrapper around U256, pads to even length by default
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ rustdoc does not generate documentation for macro invocations
|
= note: #[warn(unused_doc_comments)] on by default
= help: to document an item produced by a macro, the macro must produce the documentation as part of its expansion

warning: unused doc comment
--> evmexec/ethereum-newtypes/src/lib.rs:19:1
|
19 | /// An ethereum account address, pads to 20 byte hex representation by default
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ rustdoc does not generate documentation for macro invocations
|
= help: to document an item produced by a macro, the macro must produce the documentation as part of its expansion

warning: unused doc comment
--> evmexec/ethereum-newtypes/src/lib.rs:22:1
|
22 | /// An ethereum Hash, pads to 32 byte hex representation by default
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ rustdoc does not generate documentation for macro invocations
|
= help: to document an item produced by a macro, the macro must produce the documentation as part of its expansion

warning: 3 warnings emitted

-------------------------------- 2 ----------------------------------------------------
Compiling evmexec v0.1.0 (/home/mirkostad/Programmi/EthBMC-master/evmexec)
warning: use of deprecated associated function std::error::Error::description: use the Display impl or to_string()
--> evmexec/src/evm.rs:101:62
|
101 | Err(why) => panic!("couldn't spawn evm: {}", why.description()),
| ^^^^^^^^^^^
|
= note: #[warn(deprecated)] on by default

warning: variant is never constructed: Yes
--> evmexec/src/evm.rs:239:5
|
239 | Yes,
| ^^^
|
= note: #[warn(dead_code)] on by default

warning: 2 warnings emitted

---------------------------------------------- 3 -----------------------------------------------------------
warning: unused doc comment
--> parity_connector/src/types.rs:27:1
|
27 | /// A rust representation of an ethereum block, reduced to the fields used by ethAEG
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ rustdoc does not generate documentation for macro invocations
|
= note: #[warn(unused_doc_comments)] on by default
= help: to document an item produced by a macro, the macro must produce the documentation as part of its expansion

warning: method eth_blockNumber should have a snake case name
--> parity_connector/src/client.rs:9:12
|
9 | pub fn eth_blockNumber(&mut self) -> RpcRequest;
| ^^^^^^^^^^^^^^^ help: convert the identifier to snake case: eth_block_number
|
= note: #[warn(non_snake_case)] on by default

warning: method eth_getBlockByNumber should have a snake case name
--> parity_connector/src/client.rs:12:12
|
12 | pub fn eth_getBlockByNumber(&mut self, number: BlockSelector, as_tx: bool) -> RpcRequest;
| ^^^^^^^^^^^^^^^^^^^^ help: convert the identifier to snake case: eth_get_block_by_number

warning: method eth_getCode should have a snake case name
--> parity_connector/src/client.rs:15:12
|
15 | pub fn eth_getCode(&mut self, address: Address, number: BlockSelector) -> RpcRequest;
| ^^^^^^^^^^^ help: convert the identifier to snake case: eth_get_code

warning: method eth_getBalance should have a snake case name
--> parity_connector/src/client.rs:18:12
|
18 | pub fn eth_getBalance(&mut self, address: Address, number: BlockSelector) -> RpcRequest;
| ^^^^^^^^^^^^^^ help: convert the identifier to snake case: eth_get_balance

warning: method eth_getStorage should have a snake case name
--> parity_connector/src/client.rs:20:12
|
20 | pub fn eth_getStorage(&mut self, address: Address, number: BlockSelector) -> RpcRequest;
| ^^^^^^^^^^^^^^ help: convert the identifier to snake case: eth_get_storage

warning: 6 warnings emitted

------------------------------------------------------ 4 -----------------------------------------------------
Compiling esvm v0.1.0 (/home/mirkostad/Programmi/EthBMC-master/esvm)
warning: unnecessary braces around block return value
--> esvm/src/se/env.rs:18:9
|
18 | { Mutex::new(HashMap::new()) };
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: remove these braces
|
= note: #[warn(unused_braces)] on by default

warning: unnecessary parentheses around type
--> esvm/src/se/symbolic_state.rs:551:38
|
551 | pub fn pop1(&mut self) -> Option<(BVal)> {
| ^^^^^^ help: remove these parentheses
|
= note: #[warn(unused_parens)] on by default

warning: unnecessary braces around block return value
--> esvm/src/se/symbolic_state.rs:742:62
|
742 | static ref SAT_CACHE: RwLock<HashMap<Vec, bool>> = { RwLock::new(HashMap::new()) };
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: remove these braces

warning: use of deprecated associated function std::error::Error::description: use the Display impl or to_string()
--> esvm/src/se/expr/z3.rs:58:61
|
58 | Err(why) => panic!("couldn't spawn z3: {}", why.description()),
| ^^^^^^^^^^^
|
= note: #[warn(deprecated)] on by default

warning: cannot borrow res as mutable because it is also borrowed as immutable
--> esvm/src/se/symbolic_executor/stack_ops.rs:55:25
|
43 | &res.env.blockhashes,
| ------- immutable borrow occurs here
...
55 | res.push(Arc::clone(hash));
| ^^^ ---- immutable borrow later used here
| |
| mutable borrow occurs here
|
= note: #[warn(mutable_borrow_reservation_conflict)] on by default
= warning: this borrowing pattern was not meant to be accepted, and may become a hard error in the future
= note: for more information, see issue #59159 rust-lang/rust#59159

warning: 5 warnings emitted

-------------------------------------------------------------- 5 ---------------------------------------------------------
Compiling contracts v0.1.0 (/home/mirkostad/Programmi/EthBMC-master/esvm/contracts)
warning: unused Result that must be used
--> esvm/src/main.rs:25:5
|
25 | fs::create_dir_all("log");
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: #[warn(unused_must_use)] on by default
= note: this Result may be an Err variant, which should be handled

warning: 1 warning emitted

Then I tried to execute
$ ./target/release/ethbmc examples/rubixi/rubixi.yml
I receive the output in the attachment.
Do you have any suggestion?
Thanks in advance
rubixi_error.txt

[Joool]

Should be fixed now. Please raise another issue if the error persists.