Assertion violation at File: ../src/nlsat/nlsat_interval_set.cpp:94

[merlinsun]

Hi, For this instance, z3 https://github.com/Z3Prover/z3/commit/dd906893394344d7a68ea38f57ec83195744f81b

$ z3 small.smt2
unsat
ASSERTION VIOLATION
File: ../src/nlsat/nlsat_interval_set.cpp
Line: 94
!is_zero(s) || curr.m_upper_open || next.m_lower_open
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
s
Segmentation fault (core dumped)
$ cat small.smt2
(declare-const x1 Bool)
(declare-fun ex () Int)
(declare-fun e () Int)
(declare-fun x () Int)
(push)
(assert (forall ((E Int) (E Int) (E Int) (ex Int) (E Int)) (= 0 (+ ex e (* x)))))
(check-sat)
(pop)
(assert (or (exists ((V String)) x1) (exists ((E Int) (E Int)) (= 956 (+ (* x x x) (* e e e) (* ex ex ex))))))
(assert (exists ((e Int)) (or (= 0 e) (distinct 956 (+ ex x (* e e))))))
(check-sat)

[merlinsun]

A related instance:

$ cat delta.smt2
(declare-fun v () Int)
(declare-fun a () String)
(assert (or (distinct (str.substr a 0 0) (str.substr a 0 0)) (= (div 1 0) (div 0 (/ 0 0)))))
(assert (forall ((a Int)) (distinct 1 (mod (- (* a v 2 a)) (* a 2 v)))))
(check-sat)

[levnach]

There is no repro for either instance in d7c0e17f9617d641262bf3a5883d87556773cc5f.