From 7f7e70772d04b1c574609a5504c9160ca01aca67 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Mon, 2 Mar 2015 10:38:03 +0530
Subject: Parse Bv values

---
 Source/Provers/SMTLib/ProverInterface.cs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'Source')

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index c433e84c..320d0469 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -1996,8 +1996,11 @@ namespace Microsoft.Boogie.SMTLib
             else
                 throw new VCExprEvaluationException();
         }
-        if (resp.Name == "-" && resp.ArgCount == 1)
+        if (resp.Name == "-" && resp.ArgCount == 1) // negative int
             return Microsoft.Basetypes.BigNum.FromString("-" + resp.Arguments[0].Name);
+        if (resp.Name == "_" && resp.ArgCount == 2 && resp.Arguments[0].Name.StartsWith("bv")) // bitvector
+            return new BvConst(Microsoft.Basetypes.BigNum.FromString(resp.Arguments[0].Name.Substring("bv".Length)),
+                int.Parse(resp.Arguments[1].Name));
         if (resp.ArgCount != 0)
             throw new VCExprEvaluationException();
         if (expr.Type.Equals(Boogie.Type.Bool))
-- 
cgit v1.2.3