From 285277ada67d0536c0a7c2f8d6cc8353c3946e17 Mon Sep 17 00:00:00 2001 From: Michal Moskal Date: Mon, 22 Aug 2011 16:16:59 -0700 Subject: Use SMT2 syntax for sign_extend --- Source/Provers/SMTLib/SMTLibLineariser.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs') 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"); -- cgit v1.2.3