Rules containing the "smt-lemma" attribute are used as axioms as is, i.e. without applying functions in them. This leads to "missing SMTLib translation" errors. For e.g., in the case the case of the EVM-Semantics, the following rule -
results in a missing SMTLib translation for pow256, which could be avoided if the pow256 function was applied. @andreistefanescu @bmmoore Is this expected (in which case we just don't use the function, and document the behavior), or a bug?
Rules containing the "smt-lemma" attribute are used as axioms as is, i.e. without applying functions in them. This leads to "missing SMTLib translation" errors. For e.g., in the case the case of the EVM-Semantics, the following rule -
results in a
missing SMTLib translation for pow256
, which could be avoided if thepow256
function was applied. @andreistefanescu @bmmoore Is this expected (in which case we just don't use the function, and document the behavior), or a bug?