4 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 332b703e8..32ee2a744 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1830,6 +1830,7 @@ set(regress_1_tests
   regress1/sygus/issue3648.smt2
   regress1/sygus/issue3649.sy
   regress1/sygus/issue3802-default-consts.sy
+  regress1/sygus/issue3839-cond-rewrite.smt2
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy
diff --git a/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 b/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2
index 44f475d83..f46147d7b 100644
--- a/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2
+++ b/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --ext-rewrite-quant
+; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
 (declare-fun Q (Int Int) Bool)
diff --git a/test/regress/regress0/quantifiers/agg-rew-test.smt2 b/test/regress/regress0/quantifiers/agg-rew-test.smt2
index d1159278e..7dfb1430e 100644
--- a/test/regress/regress0/quantifiers/agg-rew-test.smt2
+++ b/test/regress/regress0/quantifiers/agg-rew-test.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --ext-rewrite-quant
+; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
 (declare-fun Q (Int Int) Bool)
diff --git a/test/regress/regress1/sygus/issue3839-cond-rewrite.smt2 b/test/regress/regress1/sygus/issue3839-cond-rewrite.smt2
new file mode 100644
index 000000000..cbe8f089d
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3839-cond-rewrite.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference
+(set-logic ALL)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(assert (xor (> a 0) (not (and (ite (= a b) (> (* 4 a b) 1) true) (> (* a a) 0)))))
+(assert (= a b))
+(assert (> (* a b) 0))
+(check-sat)
+