Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 126
    • Issues 126
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 16
    • Merge Requests 16
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
  • Why3
  • why3why3
  • Issues
  • #101

Closed
Open
Opened Mar 27, 2018 by Raphaël Rieu-Helft@rrieuhelOwner

eliminate_literal, range types and Eprover driver

On the following example, launching Eprover fails with this error message: "internal failure: Failure in transformation eliminate_literal Ident int63'axiom is already declared, with a different declaration"

The SMT solvers work fine.

module A

use import int.Int
use import mach.int.Int63

let test (x:int63) : int63
  requires { x < 100 }
= x+1

end
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#101