BV: Add missing type check for BITVECTOR_REPEAT_OP. (#4614)

Fixes #4075.

diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 42b90cd29522ccad4c94c27bda02d1fa224ac561..3589538bf76662b045ff63edb82d8fc3443450dc 100644 (file)
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -302,6 +302,10 @@ class BitVectorRepeatTypeRule
       throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
     }
     unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
+    if (repeatAmount == 0)
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting number of repeats > 0");
+    }
     return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
   }
 }; /* class BitVectorRepeatTypeRule */

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0e6fc26461db720bdb11434f77746e3d44d88d0f..f225c2ed6cb10dce311375d56c3edf9572b00012 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -360,6 +360,7 @@ set(regress_0_tests
   regress0/bv/fuzz40.smtv1.smt2
   regress0/bv/fuzz41.smtv1.smt2
   regress0/bv/issue3621.smt2
+  regress0/bv/issue-4075.smt2
   regress0/bv/issue-4130.smt2
   regress0/bv/int_to_bv_err_on_demand_1.smt2
   regress0/bv/mul-neg-unsat.smt2

diff --git a/test/regress/regress0/bv/issue-4075.smt2 b/test/regress/regress0/bv/issue-4075.smt2
new file mode 100644 (file)
index 0000000..ea1be94
--- /dev/null
+++ b/test/regress/regress0/bv/issue-4075.smt2
@@ -0,0 +1,10 @@
+; EXPECT: (error "Parse Error: issue-4075.smt2:10.26: expecting number of repeats > 0
+; EXPECT:
+; EXPECT:  (simplify ((_ repeat 0) b))
+; EXPECT:                       ^
+; EXPECT:")
+; EXIT: 1
+(set-logic QF_BV)
+(define-sort a () (_ BitVec 4))
+(declare-const b a)
+(simplify ((_ repeat 0) b))