Add multitest format

[sskeirik]

Fixes: runtimeverification/firefly-michelson#6

[ehildenb]

Things to check for the super-long build time:

• z3 --version >= 4.8.6. Check if Z3 is running for ridiculously long amounts of time.
• Also takes forever to compile haskell backend?
• Try --heuristic oqbaR : https://github.com/runtimeverification/algorand-sc-semantics/blob/master/Makefile#L245
• If there's an obvious segmentation of rules, you can use priority(...) to tell the LLVM backend to manually partition the rules.

[ehildenb]

You can use configuration fragments instead for storing state, which you can see an example of in KEVM:

    syntax InternalOp ::= "#pushCallStack"
 // --------------------------------------
    rule <k> #pushCallStack => . ... </k>
         <callStack> (.List => ListItem(<callState> CALLSTATE </callState>)) ... </callStack>
         <callState> CALLSTATE </callState>

    syntax InternalOp ::= "#popCallStack"
 // -------------------------------------
    rule <k> #popCallStack => . ... </k>
         <callStack>  (ListItem(<callState> CALLSTATE </callState>) => .List) ... </callStack>
         <callState> _ => CALLSTATE </callState>

    syntax InternalOp ::= "#dropCallStack"
 // --------------------------------------
    rule <k> #dropCallStack => . ... </k>
         <callStack> (ListItem(_) => .List) ... </callStack>

Example from KEVM: https://github.com/kframework/evm-semantics/blob/master/evm.md#the-callstack