Skip to content

Commit 45ed4c2

Browse files
CaelmBleidddenis-fokin
authored andcommitted
Replace z3 jar files with KSMT dependency (#1941)
(cherry picked from commit 88927a9)
1 parent ce29482 commit 45ed4c2

File tree

2 files changed

+17
-6
lines changed

2 files changed

+17
-6
lines changed

gradle.properties

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ junit5Version=5.8.0-RC1
2828
junit4Version=4.13.2
2929
junit4PlatformVersion=1.9.0
3030
mockitoVersion=3.5.13
31-
ksmtVersion=0.4.2
31+
ksmtVersion=0.4.3
3232
sootVersion=4.4.0-FORK-2
3333
kotlinVersion=1.7.20
3434
log4j2Version=2.13.3

utbot-framework-test/src/test/kotlin/org/utbot/examples/math/OverflowAsErrorTest.kt

Lines changed: 16 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import org.utbot.framework.plugin.api.CodegenLanguage
88
import org.utbot.testcheckers.eq
99
import org.utbot.testcheckers.withSolverTimeoutInMillis
1010
import org.utbot.testcheckers.withTreatingOverflowAsError
11-
import org.utbot.testing.AtLeast
11+
import org.utbot.testing.DoNotCalculate
1212
import org.utbot.testing.Compilation
1313
import org.utbot.testing.UtValueTestCaseChecker
1414
import org.utbot.testing.ignoreExecutionsNumber
@@ -32,12 +32,23 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
3232
checkWithException(
3333
OverflowExamples::intOverflow,
3434
eq(5),
35-
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<OverflowDetectionError>() }, // through overflow
36-
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<OverflowDetectionError>() }, // through overflow (2nd '*')
35+
{ x, _, r ->
36+
val overflowOccurred = kotlin.runCatching {
37+
Math.multiplyExact(x, x)
38+
}.isFailure
39+
overflowOccurred && r.isException<OverflowDetectionError>()
40+
}, // through overflow
41+
{ x, _, r ->
42+
val twoMul = Math.multiplyExact(x, x)
43+
val overflowOccurred = kotlin.runCatching {
44+
Math.multiplyExact(twoMul, x)
45+
}.isFailure
46+
overflowOccurred && r.isException<OverflowDetectionError>()
47+
}, // through overflow (2nd '*')
3748
{ x, _, r -> x * x * x >= 0 && x >= 0 && r.getOrNull() == 0 },
3849
{ x, y, r -> x * x * x > 0 && x > 0 && y == 10 && r.getOrNull() == 1 },
3950
{ x, y, r -> x * x * x > 0 && x > 0 && y != 10 && r.getOrNull() == 0 },
40-
coverage = AtLeast(90),
51+
coverage = DoNotCalculate
4152
)
4253
}
4354
}
@@ -258,7 +269,7 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
258269
}
259270
}
260271

261-
// Generated Kotlin code does not compile, so disabled for now
272+
// Generated Kotlin code does not compile, so disabled for now
262273
@Test
263274
@Disabled
264275
fun testQuickSort() {

0 commit comments

Comments
 (0)