Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • why3 why3
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 134
    • Issues 134
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 19
    • Merge requests 19
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • Why3
  • why3why3
  • Issues
  • #263

Closed
Open
Created Jan 31, 2019 by DAILLER Sylvain@sdaillerDeveloper

Removing Inline_trivial

Hello,

I don't understand what this transformation is used for. At first, I thought it was there for optimization but it seems that removing it from the driver makes cvc4 1.5 fail on some files (bench/ce/array_mono.mlw).

Am I misunderstanding the use of this transformation ? I think there may be a bug in the rest of the transformations used for CVC4 if not.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking