Fix printing of bvurem (#2963)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5311f1bec93c09a433824540fc6c126f01bd29ac..380004d02a50c41ababfd407eddb9f0b14131889 100644 (file)
--- 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 2f39bbb599ba1c8a4410b1acb448ac8964d8d598..307906dc3012a573c23db57b3919d25741f582d4 100644 (file)
--- 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 (file)
index 0000000..fc715a6
--- /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)