3 files changed, 22 insertions, 2 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 15dbf0df8..c8b052265 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -570,6 +570,8 @@ set(regress_0_tests
   regress0/preprocess/preprocess_14.cvc
   regress0/preprocess/preprocess_15.cvc
   regress0/print_lambda.cvc
+  regress0/printer/bv_consts_bin.smt2
+  regress0/printer/bv_consts_dec.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2
   regress0/push-pop/boolean/fuzz_14.smt2
@@ -846,10 +848,10 @@ set(regress_0_tests
   regress0/strings/type001.smt2
   regress0/strings/unsound-0908.smt2
   regress0/strings/unsound-repl-rewrite.smt2
-  regress0/sygus/array-grammar-select.sy
-  regress0/sygus/array-grammar-store.sy
   regress0/sygus/General_plus10.sy
   regress0/sygus/aig-si.sy
+  regress0/sygus/array-grammar-select.sy
+  regress0/sygus/array-grammar-store.sy
   regress0/sygus/c100.sy
   regress0/sygus/ccp16.lus.sy
   regress0/sygus/check-generic-red.sy
diff --git a/test/regress/regress0/printer/bv_consts_bin.smt2 b/test/regress/regress0/printer/bv_consts_bin.smt2
new file mode 100644
index 000000000..e5c3c2824
--- /dev/null
+++ b/test/regress/regress0/printer/bv_consts_bin.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --bv-print-consts-in-binary
+; EXPECT: sat
+; EXPECT: ((x #b0001))
+(set-option :produce-models true)
+(set-logic QF_BV)
+(declare-const x (_ BitVec 4))
+(assert (= x #b0001))
+(check-sat)
+(get-value (x))
diff --git a/test/regress/regress0/printer/bv_consts_dec.smt2 b/test/regress/regress0/printer/bv_consts_dec.smt2
new file mode 100644
index 000000000..98d95e822
--- /dev/null
+++ b/test/regress/regress0/printer/bv_consts_dec.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --no-bv-print-consts-in-binary
+; EXPECT: sat
+; EXPECT: ((x (_ bv1 4)))
+(set-option :produce-models true)
+(set-logic QF_BV)
+(declare-const x (_ BitVec 4))
+(assert (= x #b0001))
+(check-sat)
+(get-value (x))