Handle bitvectors

1 files changed, 11 insertions, 7 deletions

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index a4af7f40..327b2f70 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -110,13 +110,17 @@ void ObjectInvariant()
         if (op != null && !KnownFunctions.ContainsKey(op.Func)) {

           Function f = op.Func;

           Contract.Assert(f != null);

-          string printedName = Namer.GetQuotedName(f, f.Name);

-          Contract.Assert(printedName != null);

-

-          Contract.Assert(f.OutParams.Length == 1);

-          var argTypes = f.InParams.Cast<Variable>().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " ");

-          string decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";

-          AddDeclaration(decl);

+          

+          var builtin = SMTLibExprLineariser.ExtractBuiltin(f);

+          if (builtin == null) {

+            string printedName = Namer.GetQuotedName(f, f.Name);

+            Contract.Assert(printedName != null);

+

+            Contract.Assert(f.OutParams.Length == 1);

+            var argTypes = f.InParams.Cast<Variable>().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " ");

+            string decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";

+            AddDeclaration(decl);

+          }

           KnownFunctions.Add(f, true);

         } else {

           var lab = node.Op as VCExprLabelOp;