search

tweag / pirouette

Language-generic workbench for building static analysis
MIT License
47 stars 2 forks source link

First steps on symbolic eval of Plutus IR #108

Closed serras closed 2 years ago

serras commented 2 years ago

@VictorCMiraldo the current version fails with Exception: user error (no response from solver), do you have a clue about where this may come from?

(Some more investigation) it seems that PureSMT is working correctly, but we are sending information about data types in the wrong order.

serras commented 2 years ago

Reminder for future me: use declare-datatypes (as described in http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf) to declare all data types at once. That allow us to work around any potential recursion or dependency between them.