Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Assertion violation at diff_logic.h:575 (smt.phase_selection 5) #4116

Closed
rainoftime opened this issue Apr 27, 2020 · 0 comments
Closed

Assertion violation at diff_logic.h:575 (smt.phase_selection 5) #4116

rainoftime opened this issue Apr 27, 2020 · 0 comments

Comments

@rainoftime
Copy link
Contributor

Hi, for the following formula,

(set-logic QF_NRA)
(set-option :opt.priority box)
(set-option :smt.phase_selection 5)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const r3 Real)
(declare-const r6 Real)
(declare-const r8 Real)
(declare-const v3 Bool)
(declare-const v5 Bool)
(declare-const v10 Bool)
(assert (xor v10 v5 (= v1 true v0) v3 (> 2305258509.0 r8 r3 r6 574.4) true (xor v0 v0 v0 v1 v1 v1 v1 true v0 v1 v0) true true v0))
(minimize r3)
(minimize r8)
(check-sat)

z3 (commit 0499b6b) throws an assertion violation

ASSERTION VIOLATION
 File: ../src/smt/diff_logic.h
 Line: 575
 !is_feasible(m_edges[m_last_enabled_edge])
 (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
@rainoftime rainoftime changed the title Assertion violation at diff_logic.h (smt.phase_selection 5) Assertion violation at diff_logic.h:575 (smt.phase_selection 5) Apr 27, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant