Skip to content

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
    • Help
    • Support
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
    • Cycle Analytics
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Charts
  • Issues 86
    • Issues 86
    • List
    • Boards
    • Labels
    • Milestones
  • Merge Requests 11
    • Merge Requests 11
  • Packages
    • Packages
    • Container Registry
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Charts
  • Create a new issue
  • Commits
  • Issue Boards
  • Why3
  • why3why3
  • Issues
  • #193

Closed
Open
Opened Oct 02, 2018 by MARCHE Claude@marche
  • Report abuse
  • New issue
Report abuse New issue

usage of array.Array should not enforce polymorphic VCs

In Why3 0.88, for a program importing array.Array but wasn't using any other polymorphic types, the resulting tasks were not polymorphic and were consequently easier to discharge by SMT solvers.

Would it be possible to ignore the polymorphism of the new array type in Why3 1.0 ?

Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
0
Labels
None
Assign labels
  • View project labels
Reference: why3/why3#193