[Regressions] Use Wine for Windows builds (#8652)

This changes our build system to use Wine when we are testing a
cross-compiled Windows build. It updates the post-processing in the
regression script to remove `\r` characters and updates two regressions
to make them compatible with Windows builds.

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 3b2c18688b678c18cfe84dc904dcf1af12ce3180..d94adb44f1cefcd305661c50af55bdf92eeb9910 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -3222,12 +3222,20 @@ foreach(tester ${testers})
 endforeach()
 
 macro(cvc5_add_regression_test level file)
+  set(wrapper )
+  if(CMAKE_CROSSCOMPILING AND CMAKE_SYSTEM_NAME STREQUAL "Windows")
+    # Make wineserver persistent for 60 seconds (this is for better
+    # performance)
+    set(wrapper "wine -p=60")
+  endif()
+
   add_test(${file}
     ${run_regress_script}
     ${RUN_REGRESSION_ARGS}
     --lfsc-binary ${CMAKE_SOURCE_DIR}/deps/bin/lfscc
     --lfsc-sig-dir ${CMAKE_SOURCE_DIR}/proofs/lfsc/signatures
-    ${path_to_cvc5}/cvc5
+    ${wrapper}
+    ${path_to_cvc5}/cvc5${CMAKE_EXECUTABLE_SUFFIX}
     ${CMAKE_CURRENT_LIST_DIR}/${file})
   set_tests_properties(${file} PROPERTIES LABELS "regress${level}")
 

diff --git a/test/regress/cli/regress0/models-print-2.smt2 b/test/regress/cli/regress0/models-print-2.smt2
index 286bbc13b5c6dcd29ae34b9c60b36c845d66363f..2f4e94f83a3871dec2b923c43ffc59d3c1602bcb 100644 (file)
--- a/test/regress/cli/regress0/models-print-2.smt2
+++ b/test/regress/cli/regress0/models-print-2.smt2
@@ -1,9 +1,9 @@
 ; the purpose of this test is to verify that there is a `as` term in the output.
-; the scrubber excludes all lines without "(as @", and replaces this pattern by "AS".
+; the scrubber searches for "(as @a" patterns.
 
-; SCRUBBER: sed -e 's/.*(as @.*/AS/; /sat/d; /cardinality/d; /rep/d; /^($/d; /^)$/d'
-; EXPECT: AS
-; EXPECT: AS
+; SCRUBBER: grep -o "(as @a"
+; EXPECT: (as @a
+; EXPECT: (as @a
 (set-logic QF_UF)
 (set-option :produce-models true)
 (declare-sort Sort0 0)

diff --git a/test/regress/cli/regress0/options/help.smt2 b/test/regress/cli/regress0/options/help.smt2
index 3f0cd4a144d8918c1558ebedf309ca62308e9e9e..f6934bab4d6a7cff90fc0c39115306b27f9ea6d1 100644 (file)
--- a/test/regress/cli/regress0/options/help.smt2
+++ b/test/regress/cli/regress0/options/help.smt2
@@ -1,5 +1,5 @@
 ; DISABLE-TESTER: dump
 ; COMMAND-LINE: --help
-; SCRUBBER: grep -o "usage: cvc5"
-; EXPECT: usage: cvc5
-; EXIT: 1
\ No newline at end of file
+; SCRUBBER: grep -o "usage:"
+; EXPECT: usage:
+; EXIT: 1

diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py
index dca1af1d19fddbe02d4a637a343f6406414e12b1..d819a30d07325e283476c0cc0a7c1c5d9fa97425 100755 (executable)
--- a/test/regress/cli/run_regression.py
+++ b/test/regress/cli/run_regression.py
@@ -525,8 +525,8 @@ def run_benchmark(benchmark_info):
         output = output.decode()
     if isinstance(error, bytes):
         error = error.decode()
-    output = re.sub(r"^[ \t]*", "", output.strip(), flags=re.MULTILINE)
-    error = re.sub(r"^[ \t]*", "", error.strip(), flags=re.MULTILINE)
+    output = re.sub(r"^[ \t]*|\r", "", output.strip(), flags=re.MULTILINE)
+    error = re.sub(r"^[ \t]*|\r", "", error.strip(), flags=re.MULTILINE)
     # qemu (used for arm nightlies) emits additional error output for non-zero exit codes
     error = re.sub(r"qemu: uncaught target signal.*", "", error).strip()
     return (output, error, exit_status)