mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
Bugfix for QF_FP tactic
This commit is contained in:
parent
ca31c979fe
commit
f84d6bf5bb
|
@ -53,7 +53,7 @@ struct has_fp_to_real_predicate {
|
||||||
class has_fp_to_real_probe : public probe {
|
class has_fp_to_real_probe : public probe {
|
||||||
public:
|
public:
|
||||||
virtual result operator()(goal const & g) {
|
virtual result operator()(goal const & g) {
|
||||||
return !test<has_fp_to_real_predicate>(g);
|
return test<has_fp_to_real_predicate>(g);
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual ~has_fp_to_real_probe() {}
|
virtual ~has_fp_to_real_probe() {}
|
||||||
|
|
Loading…
Reference in a new issue