mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 22:33:40 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-06 18:46:47 -07:00
parent 5931e0d902
commit 1d724de915
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/fixplex_def.h
View file

@ -727,7 +727,6 @@ namespace polysat {
} }
#if 1
template<typename Ext> template<typename Ext>
void fixplex<Ext>::propagate_bounds(row const& r) { void fixplex<Ext>::propagate_bounds(row const& r) {
@ -755,7 +754,7 @@ namespace polysat {
} }
if (free_v != null_var) { if (free_v != null_var) {
if (c == 1) { if (free_c == 1) {
// //
// free_v in [lo_sum, hi_sum[ // free_v in [lo_sum, hi_sum[
// new_bound(r, free_v, lo_sum, hi_sum); // new_bound(r, free_v, lo_sum, hi_sum);
@ -791,7 +790,6 @@ namespace polysat {
void fixplex<Ext>::new_bound(row const& r, var_t x, numeral const& l, numeral const& h) { void fixplex<Ext>::new_bound(row const& r, var_t x, numeral const& l, numeral const& h) {
} }
#endif
template<typename Ext> template<typename Ext>
std::ostream& fixplex<Ext>::display(std::ostream& out) const { std::ostream& fixplex<Ext>::display(std::ostream& out) const {