mirror of
https://github.com/Z3Prover/z3
synced 2025-07-19 10:52:02 +00:00
na
This commit is contained in:
parent
ca18150c23
commit
a20b577b2f
1 changed files with 1 additions and 2 deletions
|
@ -236,8 +236,7 @@ namespace array {
|
||||||
* Assert
|
* Assert
|
||||||
* select(const(v), i) = v
|
* select(const(v), i) = v
|
||||||
*/
|
*/
|
||||||
bool solver::assert_select_const_axiom(app* select, app* cnst) {
|
bool solver::assert_select_const_axiom(app* select, app* cnst) {
|
||||||
|
|
||||||
++m_stats.m_num_select_const_axiom;
|
++m_stats.m_num_select_const_axiom;
|
||||||
expr* val = nullptr;
|
expr* val = nullptr;
|
||||||
VERIFY(a.is_const(cnst, val));
|
VERIFY(a.is_const(cnst, val));
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue