From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 15 Jun 2020 19:32:42 +0000 (-0700)
Subject: BV: Add missing type check for BITVECTOR_REPEAT_OP. (#4614)
X-Git-Tag: cvc5-1.0.0~3216
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3cb6e28c13a2c3ff42d68d5b5025e4b56cb2054b;p=cvc5.git

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 42b90cd29..3589538bf 100644
--- 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 0e6fc2646..f225c2ed6 100644
--- 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
index 000000000..ea1be9421
--- /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))