Symbolic term evaluation
Opened this issue · 0 comments
joom commented
Currently all term evaluation gets stuck, so we end up with terms like 1 + 1. It's not possible to prove things like P(1 + 1) |- P(2) without the Z3 rule, but it should be.
Opened this issue · 0 comments
Currently all term evaluation gets stuck, so we end up with terms like 1 + 1. It's not possible to prove things like P(1 + 1) |- P(2) without the Z3 rule, but it should be.