mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-21 11:52:05 +00:00
Code Activity

use insert_if_not_there

Browse source
This commit is contained in:
Doug Woos 2017-01-31 11:47:44 -08:00
parent 89ba99918e
commit d9e43f0e6d
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/sine_filter.cpp
View file

@ -98,8 +98,8 @@ private:
if (is_app(curr)) { if (is_app(curr)) {
app *a = to_app(curr); app *a = to_app(curr);
func_decl *f = a->get_decl(); func_decl *f = a->get_decl();
if (is_name(f) && !consts.contains(f)) { if (is_name(f)) {
consts.insert(f); consts.insert_if_not_there(f);
} }
} }
} }