From 60f999f06c74f381b88f929a924c1eed66debdd7 Mon Sep 17 00:00:00 2001
From: Azat Abdullin <azat.aam@gmail.com>
Date: Wed, 19 Jul 2023 17:56:52 +0300
Subject: [PATCH] fix random seed for SMT

---
 .../kotlin/org/vorpal/research/kex/smt/ksmt/KSMTSolver.kt | 8 +++++++-
 kex-test.ini                                              | 5 +++--
 kex.ini                                                   | 1 +
 3 files changed, 11 insertions(+), 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
index c0b5b2c13..85bdb5f66 100644
--- 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
index 5ac22f655..7cb7c2a4c 100644
--- 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
index 8904f607b..4e33c3191 100644
--- 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