mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-11 15:50:29 +00:00
Code Activity

Address code review: simplify constructor, add UNREACHABLE()

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-10 17:10:36 +00:00
parent 35addda546
commit 40b33ab353
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/seq/seq_nielsen.cpp
View file

@ -620,7 +620,7 @@ namespace seq {
nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver* solver):
m_sg(sg),
m_solver(solver ? solver : nullptr) {
m_solver(solver) {
if (!m_solver) {
m_owned_solver = alloc(lp_simple_solver, sg.get_manager());
m_solver = m_owned_solver.get();
@ -2742,6 +2742,7 @@ namespace seq {
case int_constraint_kind::ge:
return expr_ref(arith.mk_ge(ic.m_lhs, ic.m_rhs), m);
}
UNREACHABLE();
return expr_ref(m.mk_true(), m);
}