Fix file extension (#1919)

* Fix file extension

* Update Makefile

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 745183a6b041aa3eb476045543cdd3efeb9af3b7..ca22aba5f1b26c0a44e2eff9d6649beabcc0b8bb 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1806,6 +1806,7 @@ DISABLED_TESTS = \
        regress0/sets/sets-new.smt2 \
        regress0/sets/sets-testlemma-ints.smt2 \
        regress0/sets/sets-testlemma-reals.smt2 \
+       regress0/sygus/sygus-uf.sy \
        regress0/symmetric.smt \
        regress0/tptp/BOO003-4.p \
        regress0/tptp/BOO027-1.p \

diff --git a/test/regress/regress0/sygus/sygus-uf.sl b/test/regress/regress0/sygus/sygus-uf.sl
deleted file mode 100644 (file)
index 95cd877..0000000
--- a/test/regress/regress0/sygus/sygus-uf.sl
+++ /dev/null
@@ -1,20 +0,0 @@
-(set-logic LIA)
-
-(declare-fun uf (Int) Int)
-
-(synth-fun f ((x Int) (y Int)) Bool
-  ((Start Bool (true false
-                (<= IntExpr IntExpr)
-                (= IntExpr IntExpr)
-                (and Start Start)
-                (or Start Start)
-                (not Start)))
-   (IntExpr Int (0 1 x y
-                 (+ IntExpr IntExpr)
-                 (- IntExpr IntExpr)))))
-
-(declare-var x Int)
-
-(constraint (f (uf x) (uf x)))
-
-(check-synth)

diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy
new file mode 100644 (file)
index 0000000..95cd877
--- /dev/null
+++ b/test/regress/regress0/sygus/sygus-uf.sy
@@ -0,0 +1,20 @@
+(set-logic LIA)
+
+(declare-fun uf (Int) Int)
+
+(synth-fun f ((x Int) (y Int)) Bool
+  ((Start Bool (true false
+                (<= IntExpr IntExpr)
+                (= IntExpr IntExpr)
+                (and Start Start)
+                (or Start Start)
+                (not Start)))
+   (IntExpr Int (0 1 x y
+                 (+ IntExpr IntExpr)
+                 (- IntExpr IntExpr)))))
+
+(declare-var x Int)
+
+(constraint (f (uf x) (uf x)))
+
+(check-synth)