Skip to content

keep solver state in the "right" branch #3

@ruaronicola

Description

@ruaronicola

Currently there is no such thing as "cloning" in yices. This means that---whenever we fork the execution---one of the two branches will use a fresh solver, that does not benefit from incremental solving. If such branch is the only one that's NOT pruned/reverted, then the choice of giving it the fresh solver was sub-optimal, as we throw away incremental solving for no reason.

NOTE: keep in mind that this is only meaningful as long as yices devs don't implement a cloning mechanism.

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions