2 files changed, 42 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c6c55d847..58a43895e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2201,6 +2201,7 @@ set(regress_2_tests
   regress2/sygus/nia-max-square.sy
   regress2/sygus/no-syntax-test-no-si.sy
   regress2/sygus/pbe_bvurem.sy
+  regress2/sygus/policyM.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/policyM.sy b/test/regress/regress2/sygus/policyM.sy
new file mode 100644
index 000000000..0e9b33148
--- /dev/null
+++ b/test/regress/regress2/sygus/policyM.sy
@@ -0,0 +1,41 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
+(set-logic ALL)
+
+(declare-datatype Pair ((pair (pmin Int) (pmax Int))))
+
+(define-fun wf ((p Pair)) Bool
+  (<= (pmin p) (pmax p)))
+(define-fun a ((p Pair) (q Pair)) Bool
+  (< (pmax p) (pmin q)))
+(define-fun intMax ((x Int) (y Int)) Int
+  (ite (>= x y) x y))
+(define-fun intMin ((x Int) (y Int)) Int
+  (ite (>= x y) y x))
+(define-fun midpoint ((x Int) (y Int)) Int
+  (div (+ x y) 2))
+
+(synth-fun pW ((p Pair) (q Pair)) Pair
+  ((StartPair Pair) (StartInt Int)) (
+  (StartPair Pair ((pair StartInt StartInt)))
+  (StartInt Int ((pmin p) (pmax p) (pmin q) (pmax q) (intMax StartInt StartInt) (intMin StartInt StartInt) (midpoint StartInt StartInt)))
+))
+(synth-fun pL ((p Pair) (q Pair)) Pair
+  ((StartPair Pair) (StartInt Int)) (
+  (StartPair Pair ((pair StartInt StartInt)))
+  (StartInt Int ((+ StartInt StartInt) 0 1 (pmin p) (pmax p) (pmin q) (pmax q) (intMax StartInt StartInt) (intMin StartInt StartInt) (midpoint StartInt StartInt)))
+))
+
+(declare-var p Pair)
+(declare-var q Pair)
+(declare-var r Pair)
+
+(constraint (=> (and (wf p) (wf q)) (wf (pW p q))))
+(constraint (=> (and (wf p) (wf q)) (wf (pL p q))))
+
+(constraint (=> (and (wf p) (wf q) (wf r) (a p r)) (a (pW p q) r)))
+(constraint (=> (and (wf p) (wf q) (wf r) (a p r)) (a p (pL r q))))
+
+(constraint (=> (and (wf p) (wf q)) (not (a (pL q p) (pW p q)))))
+
+(check-synth)