mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 12:50:32 +00:00
Code Activity

rename

Browse source
This commit is contained in:
Jakob Rath 2023-01-24 11:12:30 +01:00
parent cf1ce4cea2
commit 7fbf27309b
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -415,19 +415,19 @@ namespace polysat {
}; };
class univariate_bitblast_factory : public univariate_solver_factory { class univariate_bitblast_factory : public univariate_solver_factory {
symbol qf_bv; symbol m_logic;
scoped_ptr<solver_factory> sf; scoped_ptr<solver_factory> m_factory;
public: public:
univariate_bitblast_factory() : univariate_bitblast_factory() :
qf_bv("QF_BV") { m_logic("QF_BV") {
sf = mk_smt_strategic_solver_factory(qf_bv); m_factory = mk_smt_strategic_solver_factory(m_logic);
} }
~univariate_bitblast_factory() override = default; ~univariate_bitblast_factory() override = default;
scoped_ptr<univariate_solver> operator()(unsigned bit_width) override { scoped_ptr<univariate_solver> operator()(unsigned bit_width) override {
return alloc(univariate_bitblast_solver, *sf, bit_width); return alloc(univariate_bitblast_solver, *m_factory, bit_width);
} }
}; };