mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Jakob Rath 2023-01-19 19:08:53 +01:00
parent 2056d392ba
commit c6cd35508b
2 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/dd/dd_pdd.h
View file

@ -561,7 +561,7 @@ namespace dd {
char const* lparen() const { return require_parens ? "(" : ""; }
char const* rparen() const { return require_parens ? ")" : ""; }
public:
val_pp(pdd_manager const& m, rational const& val, bool require_parens): m(m), val(val), require_parens(require_parens) {}
val_pp(pdd_manager const& m, rational const& val, bool require_parens = false): m(m), val(val), require_parens(require_parens) {}
std::ostream& display(std::ostream& out) const;
};

1
src/math/polysat/types.h
View file

@ -34,6 +34,7 @@ namespace polysat {
typedef dd::pdd pdd;
typedef dd::bdd bdd;
typedef dd::bddv bddv;
typedef dd::val_pp val_pp;
typedef unsigned pvar;
inline const pvar null_var = UINT_MAX;