mirror of
https://github.com/Z3Prover/z3
synced 2025-06-03 04:41:21 +00:00
fix build with gcc
This commit is contained in:
parent
f16550cf51
commit
08139d1ab1
1 changed files with 1 additions and 1 deletions
|
@ -302,7 +302,7 @@ namespace smt {
|
||||||
app_ref eq(m_manager.mk_eq(fapp, val), m_manager);
|
app_ref eq(m_manager.mk_eq(fapp, val), m_manager);
|
||||||
TRACE("assert_distinct", tout << "eq: " << mk_pp(eq, m_manager) << "\n";);
|
TRACE("assert_distinct", tout << "eq: " << mk_pp(eq, m_manager) << "\n";);
|
||||||
assert_default(eq, 0);
|
assert_default(eq, 0);
|
||||||
mark_as_relevant(eq);
|
mark_as_relevant(eq.get());
|
||||||
// TODO: we may want to hide the auxiliary values val and the function f from the model.
|
// TODO: we may want to hide the auxiliary values val and the function f from the model.
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue