diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index 0227139cf..571d19593 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -126,7 +126,15 @@ namespace polysat { } } - + inline std::ostream& operator<<(std::ostream& out, fixed_slice const& f) { + out << "fixed_slice"; + if (f.child != null_var) + out << " child v" << f.child; + out << " offset " << f.offset; + out << " length " << f.length; + out << " value " << f.value; + return out; + } inline std::ostream& operator<<(std::ostream& out, offset_slice const& js) { if (js.offset == 0)