From bc550fa115401256616042ccb7a559ec252e319b Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 May 2019 11:41:03 -0500
Subject: [PATCH] Fix printing of bvurem (#2963)

---
 src/printer/smt2/smt2_printer.cpp         |  1 +
 test/regress/CMakeLists.txt               |  1 +
 test/regress/regress2/sygus/pbe_bvurem.sy | 32 +++++++++++++++++++++++
 3 files changed, 34 insertions(+)
 create mode 100644 test/regress/regress2/sygus/pbe_bvurem.sy

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5311f1bec..380004d02 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1043,6 +1043,7 @@ static string smtKindString(Kind k, Variant v)
   case kind::BITVECTOR_NEG: return "bvneg";
   case kind::BITVECTOR_UDIV_TOTAL:
   case kind::BITVECTOR_UDIV: return "bvudiv";
+  case kind::BITVECTOR_UREM_TOTAL:
   case kind::BITVECTOR_UREM: return "bvurem";
   case kind::BITVECTOR_SDIV: return "bvsdiv";
   case kind::BITVECTOR_SREM: return "bvsrem";
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2f39bbb59..307906dc3 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1786,6 +1786,7 @@ set(regress_2_tests
   regress2/sygus/multi-udiv.sy
   regress2/sygus/nia-max-square.sy
   regress2/sygus/no-syntax-test-no-si.sy
+  regress2/sygus/pbe_bvurem.sy
   regress2/sygus/process-10-vars-2fun.sy
   regress2/sygus/process-arg-invariance.sy
   regress2/sygus/real-grammar-neg.sy
diff --git a/test/regress/regress2/sygus/pbe_bvurem.sy b/test/regress/regress2/sygus/pbe_bvurem.sy
new file mode 100644
index 000000000..fc715a645
--- /dev/null
+++ b/test/regress/regress2/sygus/pbe_bvurem.sy
@@ -0,0 +1,32 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic BV)
+(define-sort BV () (_ BitVec 8))
+(synth-fun IC ((s BV) (t BV)) Bool
+  ((Start Bool (
+     true
+     false
+     (ite Start Start Start)
+     (= (bvmul StartBv s) t)
+   ))
+   (StartBv BV (
+     s
+     t
+     #x00
+     #x01
+     #x7E
+     (bvnot  StartBv)
+     (bvmul  StartBv StartBv)
+     (bvudiv  StartBv StartBv)
+     (bvurem  StartBv StartBv)
+     (bvand  StartBv StartBv)
+   ))
+))
+(constraint (not (IC (_ bv32 8) (_ bv187 8) )))
+(constraint (not (IC (_ bv102 8) (_ bv15 8) )))
+(constraint (not (IC (_ bv92 8) (_ bv85 8) )))
+(constraint (IC (_ bv39 8) (_ bv214 8) ))
+(constraint (IC (_ bv155 8) (_ bv82 8) ))
+(constraint (IC (_ bv53 8) (_ bv98 8) ))
+(constraint (IC (_ bv41 8) (_ bv47 8) ))
+(check-synth)
-- 
2.30.2