mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-05 14:55:45 +00:00
Code Activity

Fix for QF_BV core theory detection.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-02 13:01:32 +00:00
parent 35c21779e3
commit 3f6a1eb8c5
2 changed files with 8 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/bv/bv1_blaster_tactic.cpp
View file

@ -481,8 +481,6 @@ tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) {
class is_qfbv_eq_probe : public probe {
public:
virtual result operator()(goal const & g) {
bv_rewriter rw(g.m());
if (!rw.hi_div0()) return false;
bv1_blaster_tactic t(g.m());
return t.is_target(g);