Having a single semantics will reduce the maintenance effort, though there will be differing implementations for circular control-flow
We may turn invariants into simple assertions on the LLVM backend. Symbolic variables can be given default values initially and generated using a fuzzer eventually.
Having a single semantics will reduce the maintenance effort, though there will be differing implementations for circular control-flow
We may turn invariants into simple assertions on the LLVM backend. Symbolic variables can be given default values initially and generated using a fuzzer eventually.