fix random seed for SMT

vorpal-research · Jul 19, 2023 · 60f999f · 60f999f
1 parent 681b7d0
commit 60f999f
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 3 deletions.
diff --git a/kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt b/kex-ksmt/src/main/kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt
@@ -85,6 +85,7 @@ private val printSMTLib = kexConfig.getBooleanValue("smt", "logSMTLib", false)
 private val maxArrayLength = kexConfig.getIntValue("smt", "maxArrayLength", 1000)
 private val ksmtRunners = kexConfig.getIntValue("ksmt", "runners", 4)
 private val ksmtSolvers = kexConfig.getMultipleStringValue("ksmt", "solver")
+private val ksmtSeed = kexConfig.getIntValue("ksmt", "seed", 42)
 
 @Suppress("UNCHECKED_CAST")
 @AsyncSolver("ksmt")
@@ -300,7 +301,12 @@ class KSMTSolver(
 
     private suspend fun buildSolver(): KPortfolioSolver {
         if (!currentCoroutineContext().isActive) yield()
-        return portfolioSolverManager.createPortfolioSolver(ef.ctx)
+        return portfolioSolverManager.createPortfolioSolver(ef.ctx).also {
+            it.configureAsync {
+                setIntParameter("random_seed", ksmtSeed)
+                setIntParameter("seed", ksmtSeed)
+            }
+        }
     }
 
     private fun KSMTContext.recoverBitvectorProperty(

diff --git a/kex-test.ini b/kex-test.ini
@@ -90,8 +90,8 @@ memspacing = false
 slicing = false
 
 logQuery = true
-logFormulae = true
-logSMTLib = true
+logFormulae = false
+logSMTLib = false
 
 simplifyFormulae = true
 
@@ -101,6 +101,7 @@ solver = z3
 ; solver = bitwuzla
 ; solver = yices
 runners = 8
+seed = 42
 
 [debug]
 saveInstrumentedCode = true

diff --git a/kex.ini b/kex.ini
@@ -126,6 +126,7 @@ solver = cvc5
 solver = bitwuzla
 ; solver = yices
 runners = 4
+seed = 42
 
 [view]
 dot = /usr/bin/dot