[TS PBT] Retain confirmed DSL faults before symbolic preparation

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt

@@ -177,7 +177,9 @@ class DslPropertyRunner(sourceRoots: List<Path>) {
             } else {
                 null
             }
-            val symbolic = if (engine != PropertyEngine.FAST_CHECK) {
+            val concreteViolation = concrete?.failure?.kind == PropertyFailureKind.PROPERTY
+            val shouldSearch = engine != PropertyEngine.FAST_CHECK && !concreteViolation && remainingMillis() > 0L
+            val symbolic = if (shouldSearch) {
                 search(
                     compiled = compiled,
                     directory = directory,
@@ -190,7 +192,7 @@ class DslPropertyRunner(sourceRoots: List<Path>) {
             } else {
                 null
             }
-            val replay = if (symbolic?.inputs != null) {
+            val replay = if (symbolic?.inputs != null && remainingMillis() > 0L) {
                 backend.confirmOriginalWitness(
                     property = compiled.definition,
                     candidate = symbolic.captureWitness(property = compiled.definition, sources = sources),
@@ -211,7 +213,8 @@ class DslPropertyRunner(sourceRoots: List<Path>) {
                 symbolicReplay = replay,
                 elapsedMillis = started.elapsedNow().inWholeMilliseconds,
                 budgetMillis = configuration.timeoutMillis,
-                symbolicSkippedDueToDeadline = engine != PropertyEngine.FAST_CHECK && symbolic == null,
+                symbolicSkippedDueToDeadline = engine != PropertyEngine.FAST_CHECK &&
+                    !concreteViolation && symbolic == null,
             )
         } finally {
             Files.walk(directory).use { paths ->
@@ -295,6 +298,7 @@ class DslPropertyRunner(sourceRoots: List<Path>) {
             manifest = manifest,
             mapping = mapping,
             concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT),
+            deadlineReached = { symbolicRemainingMillis() <= 0L },
             coverageFeedback = feedback,
         )
     }

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/DslBudgetRetentionTest.kt

@@ -0,0 +1,40 @@
+package org.usvm.ts.pbt.dsl
+
+import org.junit.jupiter.api.Test
+import org.usvm.ts.pbt.backend.PropertyFailureKind
+import org.usvm.ts.pbt.backend.PropertyRunConfiguration
+import org.usvm.ts.pbt.model.JsConcreteValue
+import org.usvm.ts.pbt.testResourcesRoot
+import kotlin.test.assertEquals
+import kotlin.test.assertFailsWith
+import kotlin.test.assertFalse
+import kotlin.test.assertNull
+
+class DslBudgetRetentionTest {
+    @Test
+    fun `a confirmed concrete violation avoids symbolic preparation and retains its original check`() {
+        val program = defineProperty(id = "budget.concrete-violation") {
+            val add = function<(Double, Double) -> Double>(module = "calculator.ts", exportName = "brokenAdd")
+            val a by int(min = 0, max = 0)
+            val b by int(min = 0, max = 0)
+
+            check(name = "addition") { add(a, b) equalTo (a + b) }
+        }
+        val runner = DslPropertyRunner(sourceRoots = listOf(testResourcesRoot().resolve("properties/dsl")))
+        val configuration = PropertyRunConfiguration(
+            seed = 353,
+            numRuns = 1,
+            timeoutMillis = 60_000,
+            examples = listOf(listOf(JsConcreteValue.number(0.0), JsConcreteValue.number(0.0))),
+        )
+
+        val result = runner.run(program, PropertyEngine.BOTH, configuration)
+
+        assertEquals(PropertyFailureKind.PROPERTY, result.concrete?.failure?.kind)
+        assertEquals("addition", result.concrete?.failure?.checkId)
+        assertFalse(result.symbolicSkippedDueToDeadline)
+        assertNull(result.symbolic)
+        assertNull(result.symbolicReplay)
+        assertFailsWith<DslPropertyAssertionError> { result.requireSuccess() }
+    }
+}

usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/dsl/KotlinPropertyDslTest.kt

@@ -211,8 +211,8 @@ class KotlinPropertyDslTest {
 
         assertEquals("unexpected", run.concrete?.failure?.checkId)
         assertEquals("Error", run.concrete?.failure?.errorName)
-        assertEquals("unexpected", run.symbolicReplay?.originalReplay?.failure?.checkId)
-        assertEquals(WitnessOracleOutcome.THREW, run.symbolicReplay?.candidate?.target?.expectedOutcome)
+        assertNull(run.symbolic)
+        assertNull(run.symbolicReplay)
         assertFailsWith<DslPropertyAssertionError> { run.requireSuccess() }
     }