8000 Division by constant · Issue #741 · pysmt/pysmt · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content
Division by constant #741
Open
Open
@TuomLarsen

Description

@TuomLarsen

When I try to divide an integer by a constant and use Yices as the solver, I get QF_NIA not supported error. However, the manual says on p. 5 that QF_NIA is indeed supported, except that "Division by a non-constant term is not supported." (p. 45).

Could it also be that PySMT only checks for DIVs, regardless of whether it is a division by constant or not? The situation might be similar for other solvers, I only have Z3 and Yices installed.

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

      0