mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

updated header file for arithmetic solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-18 17:21:06 -07:00
parent 0b9c9cbbce
commit 2b4ba5e170
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/arith_solver.h
View file

@ -218,6 +218,7 @@ namespace arith {
svector<euf::enode_pair> m_equalities; // asserted rows corresponding to equalities.
svector<theory_var> m_definitions; // asserted rows corresponding to definitions
svector<std::pair<euf::th_eq, bool>> m_delayed_eqs;
unsigned m_delayed_eqs_qhead = 0;
literal_vector m_asserted;
expr* m_not_handled{ nullptr };