From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 May 2019 16:41:03 +0000 (-0500)
Subject: Fix printing of bvurem (#2963)
X-Git-Tag: cvc5-1.0.0~4150
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc550fa115401256616042ccb7a559ec252e319b;p=cvc5.git

Fix printing of bvurem (#2963)
---

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)