Skip to content

Server RAM grows to the limits during symbolic-args-fail.main proof  #626

Open
@jberthold

Description

@jberthold

An interim-simplification option was added to the server to work around a problem with symbolic-args-fail.main.
Without adding that, the server would grow an enormous memory footprint during the proof. I experimented with the request in question but could not find out where exactly the memory is allocated. It is not Haskell heap data, so probably the LLVM backend allocates it somehow.

Originally posted by @jberthold in #625 (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