diff options
| author |  akashlal <unknown> | 2015-03-02 10:38:03 +0530 |
|---|---|---|
| committer | akashlal <unknown> | 2015-03-02 10:38:03 +0530 |
| commit | 7f7e70772d04b1c574609a5504c9160ca01aca67 (patch) | |
| tree | 552b43b02eeea36b1a0d09f810a2467249fe6e89 /Source | |
| parent | a1f812dcbc0f139e66a938310324d3f3365af763 (diff) | |
Parse Bv values
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 5 |
1 files changed, 4 insertions, 1 deletions
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))
|