diff options
author | 2016-06-06 23:52:08 -0600 | |
---|---|---|
committer | 2016-06-06 23:52:08 -0600 | |
commit | aef6aa03c2ec101e08ea4839003b4d61a6c06d24 (patch) | |
tree | 604742afbcbded2d5d27abaa1d95ab86859634b8 /Source/Provers | |
parent | 0c22f92b10430cd70507649b1fdae62eaffac0c9 (diff) | |
parent | 87e1e7b34261eac35869e6eff83fa57ca6268f3d (diff) |
resolving conflicts
Diffstat (limited to 'Source/Provers')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibProcess.cs | 5 | ||||
-rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 4 |
2 files changed, 4 insertions, 5 deletions
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index a2fe4d4e..9fda36e7 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -91,8 +91,8 @@ namespace Microsoft.Boogie.SMTLib // Give it a chance to exit cleanly (e.g. to flush buffers) if (!prover.WaitForExit(timeout)) { - prover.Kill(); - } + prover.Kill(); + } } catch { /* Swallow errors */ } } @@ -105,7 +105,6 @@ namespace Microsoft.Boogie.SMTLib log = log.Replace("\r", "").Replace("\n", " "); Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log); } - //Console.WriteLine(cmd); toProver.WriteLine(cmd); } diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index d7c56d90..eaed83e9 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -268,7 +268,7 @@ void ObjectInvariant() "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")"; if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$"))) { - AddDeclaration(decl); + AddDeclaration(decl); } KnownVariables.Add(node); if(declHandler != null) @@ -311,7 +311,7 @@ void ObjectInvariant() return; } - if (type.IsBool || type.IsInt || type.IsReal || type.IsFloat || type.IsBv) + if (type.IsBool || type.IsInt || type.IsReal || type.IsBv) return; CtorType ctorType = type as CtorType; |