I added a test to check that it works (aka it gets translated to valid Z3 constraints and it gets the correct anwser in at least one case XD )
WARNING: Running it on my target code I get multiple ExecutionComplete { ... result: Ok(()) } outputs before the final ExecutionComplete { ..., result: Err(Panic) } one, which is different from what happens in other (standalone) examples (but maybe this is expected?).
An implementation of
cttz
:)I added a test to check that it works (aka it gets translated to valid Z3 constraints and it gets the correct anwser in at least one case XD )
WARNING: Running it on my target code I get multiple
ExecutionComplete { ... result: Ok(()) }
outputs before the finalExecutionComplete { ..., result: Err(Panic) }
one, which is different from what happens in other (standalone) examples (but maybe this is expected?).