From: Caleb Donovick <cdonovick@users.noreply.github.com>
Date: Mon, 21 May 2018 15:29:14 +0000 (-0700)
Subject: Fix file extension (#1919)
X-Git-Tag: cvc5-1.0.0~5035
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=030480e368b0373e09aa89f68f8ae916b7fccd1b;p=cvc5.git

Fix file extension (#1919)

* Fix file extension

* Update Makefile
---

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 745183a6b..ca22aba5f 100644
--- 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
index 95cd8771e..000000000
--- 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
index 000000000..95cd8771e
--- /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)