Fixes for regressions (#3557)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7f07224e0729246aabec01993557eec1806de7cb..ab060bb314308c6a7e6d5313dcff247c59c50e69 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1264,7 +1264,6 @@ set(regress_1_tests
   regress1/nl/exp1-lb.smt2
   regress1/nl/exp_monotone.smt2
   regress1/nl/factor_agg_s.smt2
-  regress1/nl/issue3307.smt2
   regress1/nl/issue3441.smt2
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
@@ -2224,6 +2223,8 @@ set(regression_disabled_tests
   regress1/issue1048-arrays-int-real.smt2
   # times out after update to tangent planes
   regress1/nl/NAVIGATION2.smt2
+  # sat or unknown in different builds
+  regress1/nl/issue3307.smt2
   # ajreynol: disabled these since they give different error messages on
   # production and debug:
   regress1/quantifiers/macro-subtype-param.smt2

diff --git a/test/regress/regress1/sygus/node-discrete.sy b/test/regress/regress1/sygus/node-discrete.sy
index 16f7243d17651359ec971aec8c384525dddc297b..707e2c36930042e3d8b78dad23488a9d16029c2f 100644 (file)
--- a/test/regress/regress1/sygus/node-discrete.sy
+++ b/test/regress/regress1/sygus/node-discrete.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
 (set-logic ALL)
 
 (declare-datatype Packet ((P1) (P2)))