summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
authorGravatar Michal Moskal <michal@moskal.me>2011-08-22 16:16:59 -0700
committerGravatar Michal Moskal <michal@moskal.me>2011-08-22 16:16:59 -0700
commit285277ada67d0536c0a7c2f8d6cc8353c3946e17 (patch)
tree320f21da7e9cc6b986e9956dd0e93cd224fffae1 /Source/Provers
parent57f7c407df2940fbf057decefab63a74e15bb7fe (diff)
Use SMT2 syntax for sign_extend
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs6
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");