diff options
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
| -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))
|