diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-08-22 16:16:59 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-08-22 16:16:59 -0700 |
| commit | 285277ada67d0536c0a7c2f8d6cc8353c3946e17 (patch) | |
| tree | 320f21da7e9cc6b986e9956dd0e93cd224fffae1 /Source/Provers | |
| parent | 57f7c407df2940fbf057decefab63a74e15bb7fe (diff) | |
Use SMT2 syntax for sign_extend
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 3e8a3fc8..ed7beabf 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -157,9 +157,9 @@ namespace Microsoft.Boogie.SMTLib string retVal = null;
retVal = f.FindStringAttribute("bvbuiltin");
- // It used to be "sign_extend 12" in Simplify, and is "sign_extend[12]" with SMT
- if (retVal != null && retVal.StartsWith("sign_extend "))
- return retVal.Replace(" ", "[") + "]";
+ // It used to be "sign_extend 12" in Simplify, and is "(_ sign_extend 12)" with SMT
+ if (retVal != null && (retVal.StartsWith("sign_extend ") || retVal.StartsWith("zero_extend ")))
+ return "(_ " + retVal + ")";
if (retVal == null) {
retVal = f.FindStringAttribute("builtin");
|