trace Assertion violation at ../src/smt/smt_clause.cpp Line: 68

[muchang]

Hi,
For this formula:

(set-option :trace true)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () String)
(assert (xor (< a 8 (* a b)) true (< (/ c d) (str.len e) a b)))
(assert (= "bef" (str.substr e c d)))
(check-sat)

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/smt/smt_clause.cpp
Line: 68
(*cls)[i] == lits[i]
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: 9be7bda

[NikolajBjorner]

doesn't reproduce on my side