Skip to content

Lambdas don't like quantified variables in body (other than their own) #2792

Description

@nunoplopes
(assert (forall ((quant (_ BitVec 8)))
  (=
   (select (lambda ((idx (_ BitVec 8))) quant) #x01)
   #x00
  )
))
(check-sat)
(get-info :reason-unknown)

prints:

unknown
(:reason-unknown "Formulas should not contain unbound variables")

This is because it seems lambdas don't allow quantified variables in their body. Is there a fundamental reason why this is the case?

(I have a bunch of benchmarks failing on my side because I'm using lambdas to encode memcpy and memory may have quantified variables due to non-determinism)

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions