We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 458e96f commit 7a4201cCopy full SHA for 7a4201c
1 file changed
usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
@@ -25,7 +25,9 @@ fun TsContext.mkTruthyExpr(
25
val conjuncts = mutableListOf<ExprWithTypeConstraint<UBoolSort>>()
26
val possibleType = memory.types.getTypeStream(expr.asExpr(addressSort)).single() as FakeType
27
28
- scope.assert(possibleType.mkExactlyOneTypeConstraint(this@mkTruthyExpr)) // TODO add to path constraints instead
+ scope.doWithState {
29
+ pathConstraints += possibleType.mkExactlyOneTypeConstraint(this@mkTruthyExpr)
30
+ }
31
32
if (!possibleType.boolTypeExpr.isFalse) {
33
conjuncts += ExprWithTypeConstraint(
0 commit comments