Tests with complex perm expressions, fixing some problems

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -1208,7 +1208,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
                       val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2, functionRecorder = fr1, smCache = smCache2)
                       if (nonEmptyChunks.isEmpty) {
-                        assert(v1.decider.checkSmoke(true))
+                        assert(v1.decider.check(tPerm === NoPerm, 0))
                         Success()
                       } else {
                         val snap = smDef2 match {
@@ -1537,8 +1537,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
           val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2, functionRecorder = fr2)
           if (nonEmptyChunks.isEmpty) {
-            assert(v1.decider.checkSmoke(true))
-            Success()
+            //assert(v1.decider.check(permissions === NoPerm, 0))
+            val snapSort = resource match {
+              case f: ast.Field => v1.symbolConverter.toSort(f.typ)
+              case _ => sorts.Snap
+            }
+            Q(s1p, hs1.head, cHeap2, v1.decider.fresh(snapSort), v1)
           } else {
             val sm = nonEmptyChunks.head.get match {
               case ch: QuantifiedFieldChunk => ch.fvf

src/main/scala/rules/chunks/MoreCompleteExhaleSupporter.scala

@@ -265,8 +265,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
           val s1p = s1.copy(loopHeapStack = hs1.tail, h = newTopHeap2, functionRecorder = fr1)
           if (nonEmptyChunks.isEmpty){
-            assert(v1.decider.checkSmoke(true))
-            Success()
+            assert(v1.decider.check(perms === NoPerm, 0))
+            Q(s1p, hs1.head, cHeap2, None, v1)
           } else {
             Q(s1p, hs1.head, cHeap2, nonEmptyChunks.head.map(_.asInstanceOf[NonQuantifiedChunk].snap), v1)
           }

src/test/scala/SiliconTestsKInductionCondPerms.scala

@@ -0,0 +1,58 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2022 ETH Zurich.
+
+import viper.silicon.{Silicon, SiliconFrontend}
+import viper.silver.reporter.NoopReporter
+import viper.silver.testing.{LocatedAnnotation, MissingOutput, SilSuite, UnexpectedOutput}
+import viper.silver.verifier.Verifier
+
+import java.nio.file.Path
+
+class SiliconTestsKInductionCondPerms extends SilSuite {
+  private val siliconTestDirectories =
+    Seq("kinduct")
+
+  private val silTestDirectories = Seq()
+    //Seq("all",
+    //    "quantifiedpermissions", "quantifiedpredicates", "quantifiedcombinations",
+    //    "wands", "termination", "refute",
+    //    "examples")
+
+  val testDirectories: Seq[String] = siliconTestDirectories ++ silTestDirectories
+
+  override def frontend(verifier: Verifier, files: Seq[Path]): SiliconFrontend = {
+    require(files.length == 1, "tests should consist of exactly one file")
+
+    val fe = new SiliconFrontend(NoopReporter)
+    fe.init(verifier)
+    fe.reset(files.head)
+    fe
+  }
+
+  override def annotationShouldLeadToTestCancel(ann: LocatedAnnotation): Boolean = {
+    ann match {
+      case UnexpectedOutput(_, _, _, _, _, _) => true
+      case MissingOutput(_, _, _, _, _, issue) => issue != 34
+      case _ => false
+    }
+  }
+
+  val silicon: Silicon = {
+    val reporter = NoopReporter
+    val debugInfo = ("startedBy" -> "viper.silicon.SiliconTests") :: Nil
+    new Silicon(reporter, debugInfo)
+  }
+
+  def verifiers: Seq[Silicon] = Seq(silicon)
+
+  override def configureVerifiersFromConfigMap(configMap: Map[String, Any]): Unit = {
+    val args = Silicon.optionsFromScalaTestConfigMap(prefixSpecificConfigMap(configMap).getOrElse("silicon", Map()))
+    silicon.parseCommandLine(commandLineArguments ++ args :+ Silicon.dummyInputFilename)
+  }
+
+  val commandLineArguments: Seq[String] =
+    Seq("--timeout", "600" /* seconds */, "--enableMoreCompleteExhale", "--enableKInduction=1", "--conditionalizePermissions")
+}