diff options
| author |  qadeer <unknown> | 2010-09-03 03:53:43 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-09-03 03:53:43 +0000 |
| commit | 1c7071447a62379f685f3fe4e36135db3778614c (patch) | |
| tree | 1e52bb6d61281935b8adb8ef44cd1dc42bf3a57f /Source/Provers/Z3api/SafeContext.cs | |
| parent | bf02a929a654145ac2bbbd19a64ff30a0043e72a (diff) | |
bunch of fixes related to Boogie error model generation from the Z3 error model generation
Diffstat (limited to 'Source/Provers/Z3api/SafeContext.cs')
| -rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index bb09be58..76c0b957 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -301,7 +301,7 @@ namespace Microsoft.Boogie.Z3 bound.Add(Unwrap(t));
}
- Term termAst = z3.MkQuantifier(isForall, weight, z3.MkSymbol(qid), z3.MkSymbol(skolemid), unwrapPatterns.ToArray(), unwrapNoPatterns.ToArray(), bound.ToArray(), unwrapBody);
+ Term termAst = z3.MkQuantifier(isForall, weight, z3.MkSymbol(qid), z3.MkSymbol(skolemid.ToString()), unwrapPatterns.ToArray(), unwrapNoPatterns.ToArray(), bound.ToArray(), unwrapBody);
return Wrap(termAst);
}
|