From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 25 Apr 2022 21:50:14 +0000 (-0700)
Subject: [Regressions] Use Wine for Windows builds (#8652)
X-Git-Tag: cvc5-1.0.1~226
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c821125b219f3c347414896accd9bb6bdf443b6d;p=cvc5.git

[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 3b2c18688..d94adb44f 100644
--- 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 286bbc13b..2f4e94f83 100644
--- 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 3f0cd4a14..f6934bab4 100644
--- 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 dca1af1d1..d819a30d0 100755
--- 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)