Rollback cvc bv-reduction and/or fix as incorrect

UnitTestBot · Aug 15, 2024 · 899917e · 899917e
1 parent 9c1d9cf
commit 899917e
Showing 1 changed file with 2 additions and 16 deletions.
diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt
@@ -333,25 +333,11 @@ class KCvc5ExprInternalizer(
     }
 
     override fun <T : KBvSort> transform(expr: KBvReductionAndExpr<T>) = with(expr) {
-        transform(value) { value: Term ->
-            tm.mkTerm(
-                Kind.ITE,
-                tm.mkTerm(Kind.BITVECTOR_REDAND, value),
-                tm.builder { mkBitVector(1, 1) },
-                tm.builder { mkBitVector(1, 0) },
-            )
-        }
+        transform(value) { value: Term -> tm.mkTerm(Kind.BITVECTOR_REDAND, value) }
     }
 
     override fun <T : KBvSort> transform(expr: KBvReductionOrExpr<T>) = with(expr) {
-        transform(value) { value: Term ->
-            tm.mkTerm(
-                Kind.ITE,
-                tm.mkTerm(Kind.BITVECTOR_REDOR, value),
-                tm.builder { mkBitVector(1, 1) },
-                tm.builder { mkBitVector(1, 0) },
-            )
-        }
+        transform(value) { value: Term -> tm.mkTerm(Kind.BITVECTOR_REDOR, value) }
     }
 
     override fun <T : KBvSort> transform(expr: KBvAndExpr<T>) = with(expr) {