Mentions légales du service

Skip to content
Snippets Groups Projects
Closed CVC4 1.8 model Parsing error
  • View options
  • CVC4 1.8 model Parsing error

  • View options
  • Closed Issue created by Johannes Kanig

    With current master of cvc4, Why3 is unable to parse the model. The issue is cvc4 emitting declarations like this:

    ; cardinality of integer is 1
    (declare-sort integer 0)
    (declare-fun  () integer)

    Why3 is unable to parse the last line. I will propose a (unelegant) patch which ignores such lines.

    Linked items ... 0

  • Activity

    • All activity
    • Comments only
    • History only
    • Newest first
    • Oldest first
    Loading Loading Loading Loading Loading Loading Loading Loading Loading Loading