+ Trace("quant-init-debug")
+ << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
+ << options::fmfBound() << std::endl;
+ if (tr.useFmcModel())
+ {
+ Trace("quant-init-debug") << "...make fmc builder." << std::endl;
+ d_builder.reset(new fmcheck::FullModelChecker(qs, qr, qim));
+ }
+ else
+ {
+ Trace("quant-init-debug")
+ << "...make default model builder." << std::endl;
+ d_builder.reset(new QModelBuilder(qs, qr, qim));
+ }