mirror of
https://github.com/Z3Prover/z3
synced 2025-06-05 13:51:23 +00:00
fix #5107
This commit is contained in:
parent
9c716a2788
commit
0949ad26c2
1 changed files with 0 additions and 2 deletions
|
@ -60,8 +60,6 @@ void tst_model_evaluator() {
|
||||||
{
|
{
|
||||||
fi->set_else(m.mk_app(F, vI0p, vB1p));
|
fi->set_else(m.mk_app(F, vI0p, vB1p));
|
||||||
gi->set_else(m.mk_app(G, vI0p, vB1p));
|
gi->set_else(m.mk_app(G, vI0p, vB1p));
|
||||||
mdl.register_decl(g, gi);
|
|
||||||
mdl.register_decl(h, hi);
|
|
||||||
model_pp(std::cout, mdl);
|
model_pp(std::cout, mdl);
|
||||||
e = m.mk_app(h, vI0p, vB1p);
|
e = m.mk_app(h, vI0p, vB1p);
|
||||||
eval(e, v);
|
eval(e, v);
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue