diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-04-17 12:35:29 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-04-17 12:35:29 -0700 |
| commit | f82f137fe74fe6200d172b4b2751b07eb6ff34bf (patch) | |
| tree | 74eb22dfaf1c9e3ac9a4598155c238293e628b5c /Source/Provers/SMTLib/TypeDeclCollector.cs | |
| parent | 0cbc37e668f873ccda55216113e8f0abb37ebf69 (diff) | |
various changes for using unsat cores in Houdini
Diffstat (limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs')
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 05a6caf3..a4bdee51 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -164,6 +164,11 @@ void ObjectInvariant() return TypeToString(t);
}
+ public void AddFunction(Function func) {
+ if (KnownFunctions.Contains(func))
+ return;
+ KnownFunctions.Add(func);
+ }
public override bool Visit(VCExprNAry node, bool arg) {
Contract.Requires(node != null);
|