mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 04:03:39 +00:00
undo breaking commit
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
5ac3bb04ee
commit
948a1e600e
|
@ -799,7 +799,6 @@ namespace smt {
|
||||||
}
|
}
|
||||||
|
|
||||||
void theory_fpa::finalize_model(model_generator & mg) {
|
void theory_fpa::finalize_model(model_generator & mg) {
|
||||||
#if 0
|
|
||||||
ast_manager & m = get_manager();
|
ast_manager & m = get_manager();
|
||||||
proto_model & mdl = mg.get_model();
|
proto_model & mdl = mg.get_model();
|
||||||
proto_model new_model(m);
|
proto_model new_model(m);
|
||||||
|
@ -825,7 +824,6 @@ namespace smt {
|
||||||
func_interp * fi = new_model.get_func_interp(f)->copy();
|
func_interp * fi = new_model.get_func_interp(f)->copy();
|
||||||
mdl.register_decl(f, fi);
|
mdl.register_decl(f, fi);
|
||||||
}
|
}
|
||||||
#endif
|
|
||||||
}
|
}
|
||||||
|
|
||||||
void theory_fpa::display(std::ostream & out) const
|
void theory_fpa::display(std::ostream & out) const
|
||||||
|
|
Loading…
Reference in a new issue