mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add stubs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-12 17:38:16 -07:00
parent be1a1dd7c2
commit 7a6c66a085
1 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_lra.cpp
View file

@ -1626,11 +1626,6 @@ public:
unsigned old_sz = m_assume_eq_candidates.size(); unsigned old_sz = m_assume_eq_candidates.size();
unsigned num_candidates = 0; unsigned num_candidates = 0;
int start = ctx().get_random_value(); int start = ctx().get_random_value();
auto has_value = [&](theory_var v) {
if (use_nra_model())
return true;
return can_get_ivalue(v);
};
for (theory_var i = 0; i < sz; ++i) { for (theory_var i = 0; i < sz; ++i) {
theory_var v = (i + start) % sz; theory_var v = (i + start) % sz;
enode* n1 = get_enode(v); enode* n1 = get_enode(v);