Skip to content

Silicon hangs if smt code sent to Z3 isn't indented #145

Open
@viper-admin

Description

@viper-admin

Created by @alexanderjsummers on 2015-06-04 09:54

Silicon requires that multi-line constructs (such as axioms) be indented, such that only the first line is without an indent. If modifying e.g. the preamble, and this is not respected, the tool hangs waiting for an acknowledgement from Z3.

There should be some kind of timeout mechanism for this iteraction.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't workingminor

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions