mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

try vscode from github integration

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-18 11:02:02 -07:00
parent 810b9d003d
commit 1db9f9a3b5
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/model/datatype_factory.cpp
View file

@ -35,13 +35,12 @@ expr * datatype_factory::get_some_value(sort * s) {
func_decl * c = m_util.get_non_rec_constructor(s); func_decl * c = m_util.get_non_rec_constructor(s);
ptr_vector<expr> args; ptr_vector<expr> args;
unsigned num = c->get_arity(); unsigned num = c->get_arity();
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++)
args.push_back(m_model.get_some_value(c->get_domain(i))); args.push_back(m_model.get_some_value(c->get_domain(i)));
}
expr * r = m_manager.mk_app(c, args); expr * r = m_manager.mk_app(c, args);
register_value(r); register_value(r);
TRACE("datatype", tout << mk_pp(r, m_util.get_manager()) << "\n";); TRACE("datatype", tout << mk_pp(r, m_util.get_manager()) << "\n";);
return r; return r;
} }
/** /**