Only generate counterexample if the user asks for it

uuverifiers · Nov 6, 2024 · ece5829 · ece5829
1 parent 5775936
commit ece5829
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 2 deletions.
diff --git a/src/main/scala/lazabs/horn/HornWrapper.scala b/src/main/scala/lazabs/horn/HornWrapper.scala
@@ -629,6 +629,7 @@ class SymexHornWrapper(unsimplifiedClauses   : Seq[Clause],
           "--------------------------------------")
 
       symex.printInfo = lazabs.GlobalParameters.get.log
+      symex.generateCounterExample = lazabs.GlobalParameters.get.plainCEX || lazabs.GlobalParameters.get.simplifiedCEX
       symex.solve()
     }
 

diff --git a/src/main/scala/lazabs/horn/symex/Symex.scala b/src/main/scala/lazabs/horn/symex/Symex.scala
@@ -56,6 +56,10 @@ abstract class Symex[CC](iClauses:    Iterable[CC])(
   import Symex._
 
   var printInfo = false
+
+  // This might be set to true in SymexHornWrapper
+  var generateCounterExample = false
+
   def printInfo(s : String, newLine : Boolean = true) : Unit = {
     if (printInfo)
       print(s + (if (newLine) "\n" else ""))
@@ -227,7 +231,11 @@ abstract class Symex[CC](iClauses:    Iterable[CC])(
           val proverStatus = checkFeasibility(newElectron.constraint)
           if (hasContradiction(newElectron, proverStatus)) { // false :- true
             unitClauseDB.add(newElectron, (nucleus, electrons))
-            result = Right(buildCounterExample(newElectron))
+            if (generateCounterExample) {
+              result = Right(buildCounterExample(newElectron))
+            } else {
+              result = Right(DagEmpty)
+            }
           } else if (constraintIsFalse(newElectron, proverStatus)) {
             printInfo("")
             handleFalseConstraint(nucleus, electrons)
@@ -277,7 +285,11 @@ abstract class Symex[CC](iClauses:    Iterable[CC])(
                 } else toUnitClause(clause)
               unitClauseDB.add(cuc, (clause, Nil))
               if (hasContradiction(cuc, checkFeasibility(cuc.constraint))) {
-                result = Right(buildCounterExample(cuc))
+                if (generateCounterExample) {
+                  result = Right(buildCounterExample(cuc))
+                } else {
+                  result = Right(DagEmpty)
+                }
               }
             }
             if (result == null) { // none of the assertions failed, so this is SAT