Chalice: only show warning about misleading smoke warnings if there are actually smoke warnings.

1 files changed, 1 insertions, 1 deletions

diff --git a/Chalice/src/main/scala/SmokeTest.scala b/Chalice/src/main/scala/SmokeTest.scala
index 8a8f46eb..9f23d144 100644
--- a/Chalice/src/main/scala/SmokeTest.scala
+++ b/Chalice/src/main/scala/SmokeTest.scala
@@ -80,7 +80,7 @@ object SmokeTest {
     })

     

     verificationResult +

-    (if (realErrors > 0) "The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.\n" else "") + 

+    (if (realErrors > 0 && smokeTestWarnings > 0) "The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.\n" else "") + 

     smokeResult + (if (smokeResult != "") "\n" else "") +

     status

   }