Remove invalid Theta invariant parsing test

karoliineh · karoliineh · commit 766763474bfb · 2025-09-07T15:10:34.000+03:00
diff --git a/src/test/kotlin/c/CInvariantAstTest.kt b/src/test/kotlin/c/CInvariantAstTest.kt
@@ -310,13 +310,6 @@ object CInvariantAstTest {
         )
     }
 
-    @Test
-    fun test_parsing_theta_invariants() {
-        // "SV-COMP25_no-overflow/mutual_simple.yml"
-        CInvariantAst.createAst("(0 <= T0::P75988::f::q[0])")
-        CInvariantAst.createAst("(((INT_MIN == -2147483648) && (__idx_0 == 1)) || ((INT_MIN == -2147483648) && (__idx_0 == 1)) || ((INT_MIN == -2147483648) && (__idx_0 == 1) && (! ((INT_MIN == -2147483648) && (0 <= T0::P75988::f::q[0]) && (((__a_0 == T0__P75988__f__q) ? __idx_0 : 0) == ((__a_0 == T0__P75988__f__q) ? 1 : 0))))) || ((INT_MIN == -2147483648) && (__idx_0 == 1)) || ((INT_MIN == -2147483648) && (__idx_0 == 1)))")
-    }
-
     private fun legal(input: String, expectedAst: Node) {
         val actualAst = CInvariantAst.createAst(input)
         assertEquals(expectedAst, actualAst)

Original file line number	Diff line number	Diff line change
`@@ -310,13 +310,6 @@ object CInvariantAstTest {`
`310`	`310`	`)`
`311`	`311`	`}`
`312`	`312`
`313`		`- @Test`
`314`		`- fun test_parsing_theta_invariants() {`
`315`		`- // "SV-COMP25_no-overflow/mutual_simple.yml"`
`316`		`- CInvariantAst.createAst("(0 <= T0::P75988::f::q[0])")`
`317`		`- CInvariantAst.createAst("(((INT_MIN == -2147483648) && (__idx_0 == 1)) \|\| ((INT_MIN == -2147483648) && (__idx_0 == 1)) \|\| ((INT_MIN == -2147483648) && (__idx_0 == 1) && (! ((INT_MIN == -2147483648) && (0 <= T0::P75988::f::q[0]) && (((__a_0 == T0__P75988__f__q) ? __idx_0 : 0) == ((__a_0 == T0__P75988__f__q) ? 1 : 0))))) \|\| ((INT_MIN == -2147483648) && (__idx_0 == 1)) \|\| ((INT_MIN == -2147483648) && (__idx_0 == 1)))")`
`318`		`- }`
`319`		`-`
`320`	`313`	`private fun legal(input: String, expectedAst: Node) {`
`321`	`314`	`val actualAst = CInvariantAst.createAst(input)`
`322`	`315`	`assertEquals(expectedAst, actualAst)`