Skip to content
This repository has been archived by the owner on Feb 1, 2020. It is now read-only.

Function application for "smt-lemma" rules #2375

Open
msaxena2 opened this issue Nov 23, 2017 · 0 comments
Open

Function application for "smt-lemma" rules #2375

msaxena2 opened this issue Nov 23, 2017 · 0 comments

Comments

@msaxena2
Copy link
Member

msaxena2 commented Nov 23, 2017

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 -

 rule #asWordAux(N,(#uint(X)++W)) => #asWordAux(((N *Int pow256) +Int #getIntBytes(X,0,32,0)), W) [smt-lemma] 

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?

@msaxena2 msaxena2 changed the title Macro Expansion for "smt-lemma" rules. Macro Expansion for "smt-lemma" rules Nov 23, 2017
@msaxena2 msaxena2 changed the title Macro Expansion for "smt-lemma" rules Function application for "smt-lemma" rules Nov 23, 2017
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant