ASSERTION VIOLATION: File: ../src/smt/tactic/ctx_solver_simplify_tactic.cpp, Line: 143

[zhendongsu]

[546] % z3release small.smt2
sat
sat
[547] % z3debug small.smt2
sat
ASSERTION VIOLATION
File: ../src/smt/tactic/ctx_solver_simplify_tactic.cpp
Line: 143
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[548] % cat small.smt2
(set-option :nlsat.shuffle_vars true)
(set-option :smt.phase_selection 0)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(assert (let ((f (+ a 1))) (and (<= b f) (distinct (* d d) (* c c)) (= 0 (/ 1 (* a a 1))) (> e 0))))
(check-sat)
(check-sat-using (then purify-arith ctx-solver-simplify smt))

[NikolajBjorner]

sorry, when nlsat is involved, have to refer to earlier bugs

[zhendongsu]

sorry, when nlsat is involved, have to refer to earlier bugs

Okay, Nikolaj, added it to #2650, and no nlsat-related issues for now.