search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.41k stars 1.47k forks source link

Assertion violation at theory_utvpi_def.h:753 #4158

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic QF_ALIA)
(declare-fun _substvar_46_ () (Array Int Int))
(declare-fun _substvar_48_ () (Array Int Int))
(declare-fun _substvar_44_ () Int)
(set-option :smt.phase_selection 6)
(set-option :smt.arith.solver 4)
(declare-const i0 Int)
(assert (or (= (store _substvar_48_ 20 68) _substvar_46_) (xor true true true true (>= 0 (mod _substvar_44_ 433)) true true (= i0 68) false true)))
(minimize i0)
(check-sat)

z3 (commit 71e9bf10) throws an assertion violation 

ASSERTION VIOLATION
File: ../src/smt/theory_utvpi_def.h
Line: 753
m_graph.is_feasible_dbg()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
NikolajBjorner commented 4 years ago

same as the other bug