diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/json/json.cc | 17 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 5 |
2 files changed, 20 insertions, 2 deletions
diff --git a/backends/json/json.cc b/backends/json/json.cc index 4aa8046d6..42eedc606 100644 --- a/backends/json/json.cc +++ b/backends/json/json.cc @@ -52,8 +52,23 @@ struct JsonWriter string newstr = "\""; for (char c : str) { if (c == '\\') + newstr += "\\\\"; + else if (c == '"') + newstr += "\\\""; + else if (c == '\b') + newstr += "\\b"; + else if (c == '\f') + newstr += "\\f"; + else if (c == '\n') + newstr += "\\n"; + else if (c == '\r') + newstr += "\\r"; + else if (c == '\t') + newstr += "\\t"; + else if (c < 0x20) + newstr += stringf("\\u%04X", c); + else newstr += c; - newstr += c; } return newstr + "\""; } diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index e5cfcdc08..7e0d8f571 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -583,7 +583,10 @@ if aimfile is not None: if not got_topt: skip_steps = max(skip_steps, step) - num_steps = max(num_steps, step+1) + # some solvers optimize the properties so that they fail one cycle early, + # thus we check the properties in the cycle the aiger witness ends, and + # if that doesn't work, we check the cycle after that as well. + num_steps = max(num_steps, step+2) step += 1 if btorwitfile is not None: |