1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress1/sym/sym6.smt2 b/test/regress/regress1/sym/sym6.smt2
new file mode 100644
index 000000000..3da6b4cb4
--- /dev/null
+++ b/test/regress/regress1/sym/sym6.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --symmetry-detect
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(declare-fun w () Int)
+(declare-fun u () Int)
+(declare-fun v () Int)
+
+
+(assert (= (+ w y u) (+ v z)))
+
+(assert (> (+ x (* 2 y)) (+ u v)))
+
+(assert (= (- x) (- (- y))))
+
+
+
+(assert (or (< (+ x y z) 10) (> (+ v u) 10)))
+
+
+(check-sat)
+