fix #2309

NikolajBjorner · NikolajBjorner · commit e79542cc689d · 2019-05-31T07:46:11.000-07:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
@@ -46,7 +46,7 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
     std::ostringstream buffer;
     char const * data = s.is_numerical() ? "" : s.bare_str();
 
-    if (k == 0 && *data) {
+    if (k == 0 && data && *data) {
         if (s.is_numerical()) {
             return s;
         }
@@ -664,7 +664,7 @@ class smt_printer {
             if (s.is_numerical()) {
                 sz += 7;
             }
-            else {
+            else if (s.bare_str()) {
                 sz += 3 + static_cast<unsigned>(strlen(s.bare_str()));
             }
             for (unsigned i = 0; i < a->get_num_args() && sz <= m_line_length; ++i) {

Original file line number	Diff line number	Diff line change
`@@ -46,7 +46,7 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {`
`46`	`46`	`std::ostringstream buffer;`
`47`	`47`	`char const * data = s.is_numerical() ? "" : s.bare_str();`
`48`	`48`
`49`		`- if (k == 0 && *data) {`
	`49`	`+ if (k == 0 && data && *data) {`
`50`	`50`	`if (s.is_numerical()) {`
`51`	`51`	`return s;`
`52`	`52`	`}`
`@@ -664,7 +664,7 @@ class smt_printer {`
`664`	`664`	`if (s.is_numerical()) {`
`665`	`665`	`sz += 7;`
`666`	`666`	`}`
`667`		`- else {`
	`667`	`+ else if (s.bare_str()) {`
`668`	`668`	`sz += 3 + static_cast<unsigned>(strlen(s.bare_str()));`
`669`	`669`	`}`
`670`	`670`	`for (unsigned i = 0; i < a->get_num_args() && sz <= m_line_length; ++i) {`