8000 Spacer goes into an infinte loop · Issue #7 · igcontreras/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content
Spacer goes into an infinte loop #7
Open
@hgvk94

Description

@hgvk94

benchmarks:
https://github.com/chc-comp/chc-comp22-benchmarks/blob/main/LIA-Lin-Arrays/chc-LIA-Lin-Arrays_225.smt2.gz
https://github.com/chc-comp/chc-comp22-benchmarks/blob/main/LIA-Lin-Arrays/chc-LIA-Lin-Arrays_338.smt2.gz
https://github.com/chc-comp/chc-comp22-benchmarks/blob/main/LIA-Lin-Arrays/chc-LIA-Lin-Arrays_399.smt2.gz

options:
fp.spacer.global=true fp.spacer.gg.conjecture=true fp.spacer.gg.concretize=true fp.spacer.gg.subsume=true fp.xform.slice=true fp.xform.inline_linear=true fp.xform.inline_eager=true fp.xform.tail_simplifier_pve=true fp.engine=spacer fp.print_statistics=false fp.spacer.elim_aux=true fp.spacer.reach_dnf=true fp.spacer.iuc=1 fp.spacer.iuc.arith=1 fp.validate=true fp.spacer.ground_pobs=false fp.spacer.mbqi=false fp.spacer.iuc.print_farkas_stats=false fp.spacer.iuc.old_hyp_reducer=false fp.spacer.ctp=true fp.spacer.native_mbp=true fp.spacer.weak_abs=true fp.spacer.q3=true fp.spacer.q3.use_qgen=true

commit: cf8c198

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions

      0