diff --git a/regression/Makefile b/regression/Makefile
index 1243ec9a468..5c59fd6e34c 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -1,5 +1,13 @@
 
-DIRS = ansi-c cbmc cpp goto-instrument goto-analyzer cbmc-java
+DIRS = ansi-c \
+       cbmc \
+       cpp \
+       cbmc-java \
+       goto-analyzer \
+       goto-instrument \
+       test-script \
+       # Empty last line
+
 
 test:
 	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)
diff --git a/regression/ansi-c/struct6/test.desc b/regression/ansi-c/struct6/test.desc
index d97230c659f..659eb69fc00 100644
--- a/regression/ansi-c/struct6/test.desc
+++ b/regression/ansi-c/struct6/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^main.c:2:1: error: incomplete type not permitted here$
 ^CONVERSION ERROR$
diff --git a/regression/ansi-c/struct7/test.desc b/regression/ansi-c/struct7/test.desc
index 9c24052d9c5..6c926d0df3a 100644
--- a/regression/ansi-c/struct7/test.desc
+++ b/regression/ansi-c/struct7/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^main.c:4:1: error: duplicate member .*$
 ^CONVERSION ERROR$
diff --git a/regression/cbmc-concurrency/constant_prop1/test.desc b/regression/cbmc-concurrency/constant_prop1/test.desc
index 2ae90c417a8..201dc9bdb6e 100644
--- a/regression/cbmc-concurrency/constant_prop1/test.desc
+++ b/regression/cbmc-concurrency/constant_prop1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-^Generated 1 VCC(s), 0 remaining after simplification$
+^Generated 1 VCC\(s\), 0 remaining after simplification$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-concurrency/pthread_join1/test.desc b/regression/cbmc-concurrency/pthread_join1/test.desc
index 0d60be7dfd0..41b36c525bf 100644
--- a/regression/cbmc-concurrency/pthread_join1/test.desc
+++ b/regression/cbmc-concurrency/pthread_join1/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] assertion i==1: FAILURE$
 ^\[main\.assertion\.2\] assertion i==2: SUCCESS$
-^\*\* 1 of 2 failed (2 iterations)$
+^\*\* 1 of 2 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/branch3/test.desc b/regression/cbmc-cover/branch3/test.desc
index ae7869dca0b..5d9bce60ebe 100644
--- a/regression/cbmc-cover/branch3/test.desc
+++ b/regression/cbmc-cover/branch3/test.desc
@@ -3,6 +3,6 @@ main.c
 --cover branch --unwind 6
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 23 of 23 covered (100.0%)$
+^\*\* 23 of 23 covered \(100.0%\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/branch4/test.desc b/regression/cbmc-cover/branch4/test.desc
index a37182e5491..86f003eeb8e 100644
--- a/regression/cbmc-cover/branch4/test.desc
+++ b/regression/cbmc-cover/branch4/test.desc
@@ -3,6 +3,6 @@ main.c
 --cover branch
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 1 of 1 covered (100.0%)$
+^\*\* 1 of 1 covered \(100.0%\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/condition1/test.desc b/regression/cbmc-cover/condition1/test.desc
index f73b84397ee..a5945572059 100644
--- a/regression/cbmc-cover/condition1/test.desc
+++ b/regression/cbmc-cover/condition1/test.desc
@@ -13,6 +13,6 @@ main.c
 ^\[main.coverage.8] file main.c line 14 function main condition .* true: SATISFIED
 ^\[main.coverage.9] file main.c line 16 function main condition .* false: FAILED
 ^\[main.coverage.10] file main.c line 16 function main condition .* true: SATISFIED
-^\*\* 9 of 10 covered (90.0%)
+^\*\* 9 of 10 covered \(90.0%\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/cover1/test.desc b/regression/cbmc-cover/cover1/test.desc
index de6009c659d..b3fcd90f22b 100644
--- a/regression/cbmc-cover/cover1/test.desc
+++ b/regression/cbmc-cover/cover1/test.desc
@@ -6,6 +6,6 @@ main.c
 ^\[main.coverage.1] file main.c line 8 function main condition .*: SATISFIED$
 ^\[main.coverage.2] file main.c line 9 function main condition .*: SATISFIED$
 ^\[main.coverage.3] file main.c line 13 function main condition .*: FAILED$
-^\*\* 2 of 3 covered (66.7%)$
+^\*\* 2 of 3 covered \(66.7%\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/decision1/test.desc b/regression/cbmc-cover/decision1/test.desc
index 2be13d5d5f2..29dd4e08212 100644
--- a/regression/cbmc-cover/decision1/test.desc
+++ b/regression/cbmc-cover/decision1/test.desc
@@ -3,6 +3,6 @@ main.c
 --cover decision
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 2 of 2 covered (100.0%)$
+^\*\* 2 of 2 covered \(100.0%\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/location1/test.desc b/regression/cbmc-cover/location1/test.desc
index b575efbeda3..1016f7a1aea 100644
--- a/regression/cbmc-cover/location1/test.desc
+++ b/regression/cbmc-cover/location1/test.desc
@@ -8,6 +8,6 @@ main.c
 ^\[main.coverage.3\] file main.c line 13 function main block 3: SATISFIED$
 ^\[main.coverage.4\] file main.c line 15 function main block 4: FAILED$
 ^\[main.coverage.5\] file main.c line 17 function main block 5: SATISFIED$
-^\*\* 4 of 5 covered (80.0%)
+^\*\* 4 of 5 covered \(80.0%\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/location11/test.desc b/regression/cbmc-cover/location11/test.desc
index 398e9b8b36f..78e69e1e975 100644
--- a/regression/cbmc-cover/location11/test.desc
+++ b/regression/cbmc-cover/location11/test.desc
@@ -14,6 +14,6 @@ main.c
 ^\[main.coverage.9\] file main.c line 23 function main block 10: SATISFIED$
 ^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED$
 ^\[myfunc.coverage.2\] file main.c line 7 function myfunc block 2: FAILED$
-^\*\* 6 of 11 covered (54.5%)
+^\*\* 6 of 11 covered \(54.5%\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/location12/test.desc b/regression/cbmc-cover/location12/test.desc
index 8b46af0784d..1bae5a4eb12 100644
--- a/regression/cbmc-cover/location12/test.desc
+++ b/regression/cbmc-cover/location12/test.desc
@@ -10,6 +10,6 @@ main.c
 ^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
 ^\[foo.coverage.3\] file main.c line 7 function foo block 3: FAILED$
 ^\[foo.coverage.4\] file main.c line 7 function foo block 4: SATISFIED$
-^\*\* 5 of 7 covered (71.4%)
+^\*\* 5 of 7 covered \(71.4%\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/location13/test.desc b/regression/cbmc-cover/location13/test.desc
index 543be77b095..387920fa1d0 100644
--- a/regression/cbmc-cover/location13/test.desc
+++ b/regression/cbmc-cover/location13/test.desc
@@ -13,6 +13,6 @@ main.c
 ^\[foo.coverage.3\] file main.c line 11 function foo block 3: FAILED$
 ^\[foo.coverage.4\] file main.c line 12 function foo block 4: FAILED$
 ^\[foo.coverage.5\] file main.c line 12 function foo block 5: SATISFIED$
-^\*\* 5 of 10 covered (50.0%)
+^\*\* 5 of 10 covered \(50.0%\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/location14/test.desc b/regression/cbmc-cover/location14/test.desc
index f3cb25573da..52be93aeea7 100644
--- a/regression/cbmc-cover/location14/test.desc
+++ b/regression/cbmc-cover/location14/test.desc
@@ -9,6 +9,6 @@ main.c
 ^\[main.coverage.4\] file main.c line 13 function main block 4: SATISFIED$
 ^\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED$
 ^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
-^\*\* 2 of 6 covered (33.3%)
+^\*\* 2 of 6 covered \(33.3%\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/location15/test.desc b/regression/cbmc-cover/location15/test.desc
index 3fb10c3066b..4efe26c9d40 100644
--- a/regression/cbmc-cover/location15/test.desc
+++ b/regression/cbmc-cover/location15/test.desc
@@ -12,6 +12,6 @@ main.c
 ^\[main.coverage.7\] file main.c line 17 function main block 7: SATISFIED$
 ^\[foo.coverage.1\] file main.c line 6 function foo block 1: FAILED$
 ^\[foo.coverage.2\] file main.c line 7 function foo block 2: FAILED$
-^\*\* 3 of 9 covered (33.3%)
+^\*\* 3 of 9 covered \(33.3%\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/location16/test.desc b/regression/cbmc-cover/location16/test.desc
index bb81dddf43c..acb02daaf1a 100644
--- a/regression/cbmc-cover/location16/test.desc
+++ b/regression/cbmc-cover/location16/test.desc
@@ -12,6 +12,6 @@ main.c
 ^\[func.coverage.5\] file main.c line 13 function func block 5: FAILED$
 ^\[func.coverage.6\] file main.c line 15 function func block 6: FAILED$
 ^\[func.coverage.7\] file main.c line 16 function func block 7: SATISFIED$
-^\*\* 4 of 9 covered (44.4%)
+^\*\* 4 of 9 covered \(44.4%\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc
index 060d9040829..d1779e15ce6 100644
--- a/regression/cbmc-cover/mcdc1/test.desc
+++ b/regression/cbmc-cover/mcdc1/test.desc
@@ -9,7 +9,7 @@ main.c
 ^\[main.coverage.4\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$
 ^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
 ^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 10 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc10/test.desc b/regression/cbmc-cover/mcdc10/test.desc
index daf502e74af..eb5afa10812 100644
--- a/regression/cbmc-cover/mcdc10/test.desc
+++ b/regression/cbmc-cover/mcdc10/test.desc
@@ -3,11 +3,11 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
-^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && !(C != FALSE).*: SATISFIED$
-^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE.*: SATISFIED$
-^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && !\(C != FALSE\).*: SATISFIED$
+^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && !\(C != FALSE\).*: SATISFIED$
+^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE.*: SATISFIED$
+^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && !\(C != FALSE\).*: SATISFIED$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 5 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc
index 616b3249b0d..2358a5feb12 100644
--- a/regression/cbmc-cover/mcdc11/test.desc
+++ b/regression/cbmc-cover/mcdc11/test.desc
@@ -4,12 +4,12 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$
-^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$
-^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$
-^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$
-^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$
-^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\).*: SATISFIED$
+^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE.*: SATISFIED$
+^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !\(D != FALSE\).*: SATISFIED$
+^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$
+^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 6 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc
index 44e823e13c4..341ceb9da53 100644
--- a/regression/cbmc-cover/mcdc12/test.desc
+++ b/regression/cbmc-cover/mcdc12/test.desc
@@ -4,15 +4,15 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.coverage.1\] file main.c line 12 function main MC/DC independence condition `A != FALSE && B != FALSE.*: SATISFIED$
-^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$
-^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$
-^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$
-^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$
-^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$
-^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != FALSE && !(F != FALSE).*: SATISFIED$
-^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && F != FALSE.*: SATISFIED$
-^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!(E != FALSE) && !(F != FALSE).*: SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\[main.coverage.2\] file main.c line 12 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\).*: SATISFIED$
+^\[main.coverage.3\] file main.c line 12 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE.*: SATISFIED$
+^\[main.coverage.10\] file main.c line 14 function main MC/DC independence condition `C != FALSE && !\(D != FALSE\).*: SATISFIED$
+^\[main.coverage.11\] file main.c line 14 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$
+^\[main.coverage.12\] file main.c line 14 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$
+^\[main.coverage.19\] file main.c line 25 function main MC/DC independence condition `E != FALSE && !\(F != FALSE\).*: SATISFIED$
+^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && F != FALSE.*: SATISFIED$
+^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && !\(F != FALSE\).*: SATISFIED$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 10 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc13/test.desc b/regression/cbmc-cover/mcdc13/test.desc
index c7983f47aa9..85b417fa1d7 100644
--- a/regression/cbmc-cover/mcdc13/test.desc
+++ b/regression/cbmc-cover/mcdc13/test.desc
@@ -4,10 +4,10 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && C != FALSE.* SATISFIED$
-^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && !(C != FALSE).* SATISFIED$
-^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE.* SATISFIED$
-^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE.* SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && !\(C != FALSE\).* SATISFIED$
+^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && C != FALSE.* SATISFIED$
+^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE.* SATISFIED$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 6 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc
index 6778dfcc2f8..de3fd57033c 100644
--- a/regression/cbmc-cover/mcdc14/test.desc
+++ b/regression/cbmc-cover/mcdc14/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
 ^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 2 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc2/test.desc b/regression/cbmc-cover/mcdc2/test.desc
index 6c69a4144b5..7eea5938b73 100644
--- a/regression/cbmc-cover/mcdc2/test.desc
+++ b/regression/cbmc-cover/mcdc2/test.desc
@@ -7,7 +7,7 @@ main.c
 ^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$
 ^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$
 ^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 6 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc3/test.desc b/regression/cbmc-cover/mcdc3/test.desc
index d2b3fdf6627..0a531a3b9ba 100644
--- a/regression/cbmc-cover/mcdc3/test.desc
+++ b/regression/cbmc-cover/mcdc3/test.desc
@@ -3,10 +3,10 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `!(x > (unsigned int)3) && !(y < (unsigned int)5).*: SATISFIED$
-^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && !(x > (unsigned int)3).*: SATISFIED$
-^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.*: SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `!\(x > \(unsigned int\)3\) && !\(y < \(unsigned int\)5\).*: SATISFIED$
+^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && !\(x > \(unsigned int\)3\).*: SATISFIED$
+^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && x > \(unsigned int\)3.*: SATISFIED$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 4 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc4/test.desc b/regression/cbmc-cover/mcdc4/test.desc
index 9d55f2ebf19..9ed8f0e7fce 100644
--- a/regression/cbmc-cover/mcdc4/test.desc
+++ b/regression/cbmc-cover/mcdc4/test.desc
@@ -8,7 +8,7 @@ main.c
 ^\[main.coverage.3\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
 ^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
 ^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 9 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc5/test.desc b/regression/cbmc-cover/mcdc5/test.desc
index c65bbc9cd1d..7e012738b96 100644
--- a/regression/cbmc-cover/mcdc5/test.desc
+++ b/regression/cbmc-cover/mcdc5/test.desc
@@ -8,7 +8,7 @@ main.c
 ^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$
 ^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
 ^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 9 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc
index 2072ee3b94b..7f5289c868d 100644
--- a/regression/cbmc-cover/mcdc6/test.desc
+++ b/regression/cbmc-cover/mcdc6/test.desc
@@ -3,9 +3,9 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < (unsigned int)3.* false: SATISFIED$
-^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < (unsigned int)3.* true: SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* false: SATISFIED$
+^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* true: SATISFIED$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 2 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc7/test.desc b/regression/cbmc-cover/mcdc7/test.desc
index 78af58eaf8d..7df603190cd 100644
--- a/regression/cbmc-cover/mcdc7/test.desc
+++ b/regression/cbmc-cover/mcdc7/test.desc
@@ -7,7 +7,7 @@ main.c
 ^\[main.coverage.2\] file main.c line 8 function main decision/condition `x \* 123 > 100.* true: SATISFIED$
 ^\[main.coverage.3\] file main.c line 8 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
 ^\[main.coverage.4\] file main.c line 8 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 2 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc
index bf8dabbfa0f..f1711f5c8d1 100644
--- a/regression/cbmc-cover/mcdc8/test.desc
+++ b/regression/cbmc-cover/mcdc8/test.desc
@@ -3,11 +3,11 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !(b != FALSE).* SATISFIED$
-^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && b != FALSE.* SATISFIED$
-^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && !(b != FALSE).* SATISFIED$
-^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(c != FALSE) && a != FALSE && !(b != FALSE).* SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !\(b != FALSE\).* SATISFIED$
+^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && b != FALSE.* SATISFIED$
+^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$
+^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 6 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc
index d8ec7ea5f82..3dbd096e9be 100644
--- a/regression/cbmc-cover/mcdc9/test.desc
+++ b/regression/cbmc-cover/mcdc9/test.desc
@@ -3,12 +3,12 @@ main.c
 --cover mcdc
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$
-^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && D != FALSE && A != FALSE && !(B != FALSE).* SATISFIED$
-^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE) && A != FALSE && !(B != FALSE).* SATISFIED$
-^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE && !(D != FALSE).* SATISFIED$
-^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$
-^\*\* .* of .* covered (100.0%)$
+^\[main.coverage.9\] file main.c line 16 function main MC/DC independence condition `A != FALSE && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$
+^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE && A != FALSE && !\(B != FALSE\).* SATISFIED$
+^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\) && A != FALSE && !\(B != FALSE\).* SATISFIED$
+^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE && !\(D != FALSE\).* SATISFIED$
+^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$
+^\*\* .* of .* covered \(100.0%\)$
 ^\*\* Used 8 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/LocalVarTable2/test.desc b/regression/cbmc-java/LocalVarTable2/test.desc
index 1e982eeac10..9e12f63756c 100644
--- a/regression/cbmc-java/LocalVarTable2/test.desc
+++ b/regression/cbmc-java/LocalVarTable2/test.desc
@@ -4,4 +4,4 @@ LocalVarTable2.class
 ^EXIT=0$
 ^SIGNAL=0$
 --
-return_value.*(void \*)i
+return_value.*\(void \*\)i
diff --git a/regression/cbmc-java/NullPointer1/test.desc b/regression/cbmc-java/NullPointer1/test.desc
index 0394ce544f3..d479356875a 100644
--- a/regression/cbmc-java/NullPointer1/test.desc
+++ b/regression/cbmc-java/NullPointer1/test.desc
@@ -3,7 +3,7 @@ NullPointer1.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer1.java line 16 function java::NullPointer1.main:(\[Ljava/lang/String;)V$
+^  file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/NullPointer2/test.desc b/regression/cbmc-java/NullPointer2/test.desc
index 3be1eaa44fc..366d28f8b02 100644
--- a/regression/cbmc-java/NullPointer2/test.desc
+++ b/regression/cbmc-java/NullPointer2/test.desc
@@ -3,7 +3,7 @@ NullPointer2.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V
+^  file NullPointer2.java line 9 function java::NullPointer2.main:\(\[Ljava/lang/String;\)V
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/NullPointer3/test.desc b/regression/cbmc-java/NullPointer3/test.desc
index f4956e75540..cc33c21738b 100644
--- a/regression/cbmc-java/NullPointer3/test.desc
+++ b/regression/cbmc-java/NullPointer3/test.desc
@@ -3,7 +3,7 @@ NullPointer3.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer3.java line 5 function java::NullPointer3.main:(\[Ljava/lang/String;)V bytecode_index 1$
+^  file NullPointer3.java line 5 function java::NullPointer3.main:\(\[Ljava/lang/String;\)V bytecode_index 1$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/NullPointer4/test.desc b/regression/cbmc-java/NullPointer4/test.desc
index 653f7cf47bd..2e1b728c1fc 100644
--- a/regression/cbmc-java/NullPointer4/test.desc
+++ b/regression/cbmc-java/NullPointer4/test.desc
@@ -3,7 +3,7 @@ NullPointer4.class
 --pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer4.java line 6 function java::NullPointer4.main:(\[Ljava/lang/String;)V$
+^  file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/VarLengthArrayTrace1/test.desc b/regression/cbmc-java/VarLengthArrayTrace1/test.desc
index 74403444d22..14ee7eb85a8 100644
--- a/regression/cbmc-java/VarLengthArrayTrace1/test.desc
+++ b/regression/cbmc-java/VarLengthArrayTrace1/test.desc
@@ -7,4 +7,4 @@ dynamic_3_array\[1l\]=10
 --
 ^warning: ignoring
 assignment removed
-irep("(\\"nil\\")")
+irep\("\(\\"nil\\"\)"\)
diff --git a/regression/cbmc-java/enum1/test.desc b/regression/cbmc-java/enum1/test.desc
index 8a395386017..d9ca7a162db 100644
--- a/regression/cbmc-java/enum1/test.desc
+++ b/regression/cbmc-java/enum1/test.desc
@@ -3,6 +3,6 @@ enum1.class
 --java-unwind-enum-static --unwind 3
 ^EXIT=10$
 ^SIGNAL=0$
-^Unwinding loop java::enum1.<clinit>:()V.0 iteration 5 (6 max) file enum1.java line 6 function java::enum1.<clinit>:()V bytecode_index 78 thread 0$
+^Unwinding loop java::enum1.<clinit>:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.<clinit>:\(\)V bytecode_index 78 thread 0$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/jar-file1/test.desc b/regression/cbmc-java/jar-file1/test.desc
index b50d83b8645..2e8294c7276 100644
--- a/regression/cbmc-java/jar-file1/test.desc
+++ b/regression/cbmc-java/jar-file1/test.desc
@@ -1,8 +1,8 @@
 CORE
 some_jar.jar
 
-^EXIT=\(0\|6\)$
+^EXIT=(0|6)$
 ^SIGNAL=0$
-^\(VERIFICATION SUCCESSFUL\|No support for reading JAR files\)$
+^(VERIFICATION SUCCESSFUL|No support for reading JAR files)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/jar-file2/test.desc b/regression/cbmc-java/jar-file2/test.desc
index fb9e05dad2c..2cad29df307 100644
--- a/regression/cbmc-java/jar-file2/test.desc
+++ b/regression/cbmc-java/jar-file2/test.desc
@@ -1,8 +1,8 @@
 CORE
 jar-file2.jar
 --main-class some_class
-^EXIT=\(10\|6\)$
+^EXIT=(10|6)$
 ^SIGNAL=0$
-^\(VERIFICATION FAILED\|No support for reading JAR files\)$
+^(VERIFICATION FAILED|No support for reading JAR files)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/jsr1/test.desc b/regression/cbmc-java/jsr1/test.desc
index abcbe1427a1..faec2ddbb03 100644
--- a/regression/cbmc-java/jsr1/test.desc
+++ b/regression/cbmc-java/jsr1/test.desc
@@ -4,5 +4,5 @@ edu/emory/mathcs/backport/java/util/concurrent/ConcurrentHashMap.class
 ^EXIT=0$
 ^SIGNAL=0$
 --
-\\"statement\\" (\\"jsr\\")
-\\"statement\\" (\\"ret\\")
+\\"statement\\" \(\\"jsr\\"\)
+\\"statement\\" \(\\"ret\\"\)
diff --git a/regression/cbmc-java/jsr2/test.desc b/regression/cbmc-java/jsr2/test.desc
index 0fd8981318e..844d0c49668 100644
--- a/regression/cbmc-java/jsr2/test.desc
+++ b/regression/cbmc-java/jsr2/test.desc
@@ -9,5 +9,5 @@ Labels: pc9
 Labels: pc12
 Labels: pc13
 --
-\\"statement\\" (\\"jsr\\")
-\\"statement\\" (\\"ret\\")
+\\"statement\\" \(\\"jsr\\"\)
+\\"statement\\" \(\\"ret\\"\)
diff --git a/regression/cbmc-java/package_friendly1/test.desc b/regression/cbmc-java/package_friendly1/test.desc
index 108ea5defb1..527f5b9bfe0 100644
--- a/regression/cbmc-java/package_friendly1/test.desc
+++ b/regression/cbmc-java/package_friendly1/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.class
 package_friendly1.class package_friendly2.class --show-goto-functions
-^main[.]main[(][)].*$
-^package_friendly2[.]operation2[(][)].*$
+^main[.]main[\(][\)].*$
+^package_friendly2[.]operation2[\(][\)].*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc-with-incr/BV_Arithmetic3/test.desc b/regression/cbmc-with-incr/BV_Arithmetic3/test.desc
index 4e0ad61997b..d2a7e3e7574 100644
--- a/regression/cbmc-with-incr/BV_Arithmetic3/test.desc
+++ b/regression/cbmc-with-incr/BV_Arithmetic3/test.desc
@@ -3,7 +3,7 @@ main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-\(Starting CEGAR Loop\|^Generated 1 VCC(s), 0 remaining after simplification$\)
+(Starting CEGAR Loop|^Generated 1 VCC\(s\), 0 remaining after simplification$)
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Fixedbv4/test.desc b/regression/cbmc-with-incr/Fixedbv4/test.desc
index 967f48cfce8..a43bbd7df65 100644
--- a/regression/cbmc-with-incr/Fixedbv4/test.desc
+++ b/regression/cbmc-with-incr/Fixedbv4/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-\(Starting CEGAR Loop\|VCC(s), 0 remaining after simplification$\)
+(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc
index 8b9ef5dc26b..d8033224594 100644
--- a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc
+++ b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc
@@ -3,8 +3,8 @@ main.c
 --unwind-max 3 --no-unwinding-assertions --all-properties
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.1\] assertion matriz\[(signed long int)j\]\[(signed long int)k\] <= maior: OK$
-^\[main\.assertion\.2\] assertion matriz\[(signed long int)0\]\[(signed long int)0\] < maior: FAILED$
-^\*\* 1 of 2 failed (2 iterations)$
+^\[main\.assertion\.1\] assertion matriz\[\(signed long int\)j\]\[\(signed long int\)k\] <= maior: OK$
+^\[main\.assertion\.2\] assertion matriz\[\(signed long int\)0\]\[\(signed long int\)0\] < maior: FAILED$
+^\*\* 1 of 2 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
index d0e938b109c..cf4a284351e 100644
--- a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
+++ b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.2\] .*: FAILED$
-^\*\* 1 of 2 failed (2 iterations)$
+^\*\* 1 of 2 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc
index d40554751e7..b2bf0ea5879 100644
--- a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc
+++ b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILED$
-^\*\* 1 of 9 failed (2 iterations)$
+^\*\* 1 of 9 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc
index 0215dfc4361..a2ae3807cab 100644
--- a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc
+++ b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
-^\*\* 1 of 9 failed (2 iterations)$
+^\*\* 1 of 9 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/pipe1/test.desc b/regression/cbmc-with-incr/pipe1/test.desc
index 4f3dc3ca6c6..95e607f531d 100644
--- a/regression/cbmc-with-incr/pipe1/test.desc
+++ b/regression/cbmc-with-incr/pipe1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.4\] assertion data\[1\]==31: FAILED$
-^\*\* 1 of 5 failed (2 iterations)$
+^\*\* 1 of 5 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/BV_Arithmetic3/test.desc b/regression/cbmc/BV_Arithmetic3/test.desc
index 4e0ad61997b..d2a7e3e7574 100644
--- a/regression/cbmc/BV_Arithmetic3/test.desc
+++ b/regression/cbmc/BV_Arithmetic3/test.desc
@@ -3,7 +3,7 @@ main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-\(Starting CEGAR Loop\|^Generated 1 VCC(s), 0 remaining after simplification$\)
+(Starting CEGAR Loop|^Generated 1 VCC\(s\), 0 remaining after simplification$)
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Fixedbv4/test.desc b/regression/cbmc/Fixedbv4/test.desc
index 967f48cfce8..a43bbd7df65 100644
--- a/regression/cbmc/Fixedbv4/test.desc
+++ b/regression/cbmc/Fixedbv4/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-\(Starting CEGAR Loop\|VCC(s), 0 remaining after simplification$\)
+(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc
index 6271e2d1865..9e34fa7f422 100644
--- a/regression/cbmc/Malloc23/test.desc
+++ b/regression/cbmc/Malloc23/test.desc
@@ -5,8 +5,8 @@ main.c
 ^SIGNAL=0$
 pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in \*p: FAILURE
-pointer outside dynamic object bounds in p2\[(signed long int)1\]: FAILURE
-pointer outside dynamic object bounds in p2\[(signed long int)0\]: FAILURE
-\*\* 4 of 36 failed (3 iterations)
+pointer outside dynamic object bounds in p2\[\(signed long int\)1\]: FAILURE
+pointer outside dynamic object bounds in p2\[\(signed long int\)0\]: FAILURE
+\*\* 4 of 36 failed \(3 iterations\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc
index 97ebee19e43..101a4c0e3bf 100644
--- a/regression/cbmc/Multi_Dimensional_Array6/test.desc
+++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] : SUCCESS$
 ^\[main\.assertion\.2\] : FAILURE$
-^\*\* 1 of 2 failed (2 iterations)$
+^\*\* 1 of 2 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Overflow_Addition1/test.desc b/regression/cbmc/Overflow_Addition1/test.desc
index 07fa8a17ceb..850b22d1a46 100644
--- a/regression/cbmc/Overflow_Addition1/test.desc
+++ b/regression/cbmc/Overflow_Addition1/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --signed-overflow-check
 ^SIGNAL=0$
-^\[.*\] arithmetic overflow on signed + in .*: FAILURE$
+^\[.*\] arithmetic overflow on signed \+ in .*: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc
index 32cb3052579..888430312a7 100644
--- a/regression/cbmc/Pointer_byte_extract2/test.desc
+++ b/regression/cbmc/Pointer_byte_extract2/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.2\] .*: FAILURE$
-^\*\* 1 of 2 failed (2 iterations)$
+^\*\* 1 of 2 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc
index ffd4b6e5750..8c70c85ee47 100644
--- a/regression/cbmc/Pointer_byte_extract5/test.desc
+++ b/regression/cbmc/Pointer_byte_extract5/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 11 failed (2 iterations)
+\*\* 1 of 11 failed \(2 iterations\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc
index a02bd08c46e..801d41ee41b 100644
--- a/regression/cbmc/Pointer_byte_extract8/test.desc
+++ b/regression/cbmc/Pointer_byte_extract8/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
-^\*\* 1 of 9 failed (2 iterations)$
+^\*\* 1 of 9 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
index 89b2bd695c6..5b4797b9b00 100644
--- a/regression/cbmc/Quantifiers-assertion/test.desc
+++ b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -9,5 +9,5 @@ main.c
 ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
 ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
 
-^\*\* 2 of 6 failed (2 iterations)$
+^\*\* 2 of 6 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
index 97aa2540147..cfc835ce948 100644
--- a/regression/cbmc/Quantifiers-assignment/test.desc
+++ b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -7,5 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion z1: SUCCESS$
 ^\[main.assertion.4\] assertion z2: SUCCESS$
 
-^\*\* 1 of 4 failed (2 iterations)$
+^\*\* 1 of 4 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc
index 70d08657075..5682d588b9c 100644
--- a/regression/cbmc/Quantifiers-copy/test.desc
+++ b/regression/cbmc/Quantifiers-copy/test.desc
@@ -8,5 +8,5 @@ main.c
 ^\[main.assertion.4\] assertion b\[.*\] == 3: SUCCESS$
 ^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$
 
-^\*\* 0 of 5 failed (1 iteration)$
+^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc
index 85382ac5ad0..e121e2e1955 100644
--- a/regression/cbmc/Quantifiers-if/test.desc
+++ b/regression/cbmc/Quantifiers-if/test.desc
@@ -8,5 +8,5 @@ main.c
 ^\[main.assertion.4\] failure 3: FAILURE$
 ^\[main.assertion.5\] success 2: SUCCESS$
 
-^\*\* 3 of 5 failed (2 iterations)$
+^\*\* 3 of 5 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc
index 4ebb8bc2d51..b10b600c308 100644
--- a/regression/cbmc/Quantifiers-initialisation/test.desc
+++ b/regression/cbmc/Quantifiers-initialisation/test.desc
@@ -8,5 +8,5 @@ main.c
 ^\[main.assertion.4\] assertion a\[.*\] == 4: SUCCESS$
 ^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$
 
-^\*\* 0 of 5 failed (1 iteration)$
+^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc
index ecf508fe2f7..ad5913e4d92 100644
--- a/regression/cbmc/Quantifiers-initialisation2/test.desc
+++ b/regression/cbmc/Quantifiers-initialisation2/test.desc
@@ -8,5 +8,5 @@ main.c
 ^\[main.assertion.4\] forall c\[\]: SUCCESS$
 ^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
 
-^\*\* 1 of 5 failed (2 iterations)$
+^\*\* 1 of 5 failed \(2 iterations\)$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
index e150f4a9e20..e38af4ddbdb 100644
--- a/regression/cbmc/Quantifiers-invalid-var-range/test.desc
+++ b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
@@ -3,5 +3,5 @@ main.c
 
 ^\*\* Results:$
 
-^\*\* 0 of 1 failed (1 iteration)$
+^\*\* 0 of 1 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc
index 3d9c805336a..51feeae3b08 100644
--- a/regression/cbmc/Quantifiers-not-exists/test.desc
+++ b/regression/cbmc/Quantifiers-not-exists/test.desc
@@ -3,11 +3,11 @@ main.c
 
 ^\*\* Results:$
 ^\[main.assertion.1\] assertion a\[.*\]\[.*\] > 10: SUCCESS$
-^\[main.assertion.2\] assertion tmp_if_expr$3: SUCCESS$
-^\[main.assertion.3\] assertion tmp_if_expr$6: SUCCESS$
-^\[main.assertion.4\] assertion tmp_if_expr$9: SUCCESS$
-^\[main.assertion.5\] assertion tmp_if_expr$12: SUCCESS$
-^\[main.assertion.6\] assertion tmp_if_expr$15: SUCCESS$
+^\[main.assertion.2\] assertion tmp_if_expr\$3: SUCCESS$
+^\[main.assertion.3\] assertion tmp_if_expr\$6: SUCCESS$
+^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$
+^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
+^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
 
-^\*\* 0 of 6 failed (1 iteration)$
+^\*\* 0 of 6 failed \(1 iteration\)$
 ^\VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc
index 8e763e9aa72..b1b6a0d1d60 100644
--- a/regression/cbmc/Quantifiers-not/test.desc
+++ b/regression/cbmc/Quantifiers-not/test.desc
@@ -8,5 +8,5 @@ main.c
 ^\[main.assertion.4\] success 3: SUCCESS$
 ^\[main.assertion.5\] failure 2: FAILURE$
 
-^\*\* 2 of 5 failed (2 iterations)$
+^\*\* 2 of 5 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc
index 32ab527b42f..2874b9dc0eb 100644
--- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc
+++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc
@@ -6,7 +6,7 @@ main.c
 ^\[main.assertion.2\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
-^\[main.assertion.5\] assertion tmp_if_expr$3: SUCCESS$
+^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
 
-^\*\* 0 of 5 failed (1 iteration)$
+^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
index ee061c91c3b..3bc8a8d2a5f 100644
--- a/regression/cbmc/Quantifiers-type/test.desc
+++ b/regression/cbmc/Quantifiers-type/test.desc
@@ -2,8 +2,8 @@ CORE
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] assertion tmp_if_expr$1: FAILURE$
-^\[main.assertion.2\] assertion tmp_if_expr$2: SUCCESS$
+^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
+^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
 
-^\*\* 1 of 2 failed (2 iterations)$
+^\*\* 1 of 2 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/null3/test.desc b/regression/cbmc/null3/test.desc
index 7d1a2a85c81..60ac44fc4e0 100644
--- a/regression/cbmc/null3/test.desc
+++ b/regression/cbmc/null3/test.desc
@@ -3,7 +3,7 @@ main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^Generated .* VCC(s), 0 remaining after simplification$
+^Generated .* VCC\(s\), 0 remaining after simplification$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/pipe1/test.desc b/regression/cbmc/pipe1/test.desc
index a18dce04f12..26a7b98287a 100644
--- a/regression/cbmc/pipe1/test.desc
+++ b/regression/cbmc/pipe1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.4\] assertion data\[1\]==31: FAILURE$
-^\*\* 1 of 5 failed (2 iterations)$
+^\*\* 1 of 5 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_01_19/test.desc b/regression/cegis/cegis_danger_benchmark_01_19/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_01_19/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_01_19/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_02_20/test.desc b/regression/cegis/cegis_danger_benchmark_02_20/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_02_20/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_02_20/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_03_21/test.desc b/regression/cegis/cegis_danger_benchmark_03_21/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_03_21/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_03_21/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_04_23/test.desc b/regression/cegis/cegis_danger_benchmark_04_23/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_04_23/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_04_23/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_05_24/test.desc b/regression/cegis/cegis_danger_benchmark_05_24/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_05_24/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_05_24/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_06_25/test.desc b/regression/cegis/cegis_danger_benchmark_06_25/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_06_25/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_06_25/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_11_33/test.desc b/regression/cegis/cegis_danger_benchmark_11_33/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_11_33/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_11_33/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_17_40/test.desc b/regression/cegis/cegis_danger_benchmark_17_40/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_17_40/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_17_40/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_18_41/test.desc b/regression/cegis/cegis_danger_benchmark_18_41/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_18_41/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_18_41/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_19_42/test.desc b/regression/cegis/cegis_danger_benchmark_19_42/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_19_42/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_19_42/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_20_43/test.desc b/regression/cegis/cegis_danger_benchmark_20_43/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_20_43/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_20_43/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_10/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_10/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_10/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_10/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_1000003/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_1000003/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_1000003/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_const_false-unreach-call1_1000003/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_const_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_const_true-unreach-call1/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_const_true-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_const_true-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call1/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call2/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call2/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_false-unreach-call2/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call1/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call2/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call2/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_diamond_true-unreach-call2/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_for_bounded_loop1_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_for_bounded_loop1_false-unreach-call_true-termination/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_for_bounded_loop1_false-unreach-call_true-termination/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_for_bounded_loop1_false-unreach-call_true-termination/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_functions_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_functions_false-unreach-call1/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_functions_false-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_functions_false-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_functions_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_functions_true-unreach-call1/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_functions_true-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_functions_true-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1_100/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1_100/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1_100/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_false-unreach-call1_100/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_true-unreach-call1/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_multivar_true-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_multivar_true-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_overflow_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_overflow_false-unreach-call1/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_overflow_false-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_overflow_false-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_overflow_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_overflow_true-unreach-call1/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_overflow_true-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_overflow_true-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call1/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call2/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call2/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_phases_false-unreach-call2/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call1/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call2/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call2/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_phases_true-unreach-call2/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call1/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call2/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call2/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call2/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call3/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call3/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call3/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call3/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call4/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call4/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call4/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_false-unreach-call4/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call1/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call2/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call2/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call2/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call3/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call3/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call3/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call3/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call4/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call4/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call4/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_simple_true-unreach-call4/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_false-unreach-call_true-termination/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_false-unreach-call_true-termination/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_false-unreach-call_true-termination/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_sum04_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_sum04_false-unreach-call_true-termination/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_sum04_false-unreach-call_true-termination/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_sum04_false-unreach-call_true-termination/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination_1000003/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination_1000003/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination_1000003/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_terminator_03_false-unreach-call_true-termination_1000003/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_trex02_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_trex02_false-unreach-call_true-termination/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_trex02_false-unreach-call_true-termination/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_trex02_false-unreach-call_true-termination/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_trex03_false-unreach-call_true-termination/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_trex03_false-unreach-call_true-termination/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_trex03_false-unreach-call_true-termination/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_trex03_false-unreach-call_true-termination/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call1/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call2/test.desc
index c1747971a06..f57dcb6d0a1 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call2/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_false-unreach-call2/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call1/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call1/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call1/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call1/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call2/test.desc b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call2/test.desc
index 59aa0bcc847..b81a22e5b16 100644
--- a/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call2/test.desc
+++ b/regression/cegis/cegis_danger_benchmark_svcomp_underapprox_true-unreach-call2/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_unit_2x0/test.desc b/regression/cegis/cegis_danger_unit_2x0/test.desc
index 3d7cfc3d517..14f8e34538d 100644
--- a/regression/cegis/cegis_danger_unit_2x0/test.desc
+++ b/regression/cegis/cegis_danger_unit_2x0/test.desc
@@ -3,8 +3,8 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)]x *- *DANGER_CONSTANT_2u;$
-^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[(]unsigned *int[)]x;$
-^.*__CPROVER_danger_S0_x_0 *= *[(]unsigned *int[)]x *<< *[(]unsigned *int[)]x;$
+^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)]x *- *DANGER_CONSTANT_2u;$
+^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[\(]unsigned *int[\)]x;$
+^.*__CPROVER_danger_S0_x_0 *= *[\(]unsigned *int[\)]x *<< *[\(]unsigned *int[\)]x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_unit_full1/test.desc b/regression/cegis/cegis_danger_unit_full1/test.desc
index 3d7cfc3d517..14f8e34538d 100644
--- a/regression/cegis/cegis_danger_unit_full1/test.desc
+++ b/regression/cegis/cegis_danger_unit_full1/test.desc
@@ -3,8 +3,8 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)]x *- *DANGER_CONSTANT_2u;$
-^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[(]unsigned *int[)]x;$
-^.*__CPROVER_danger_S0_x_0 *= *[(]unsigned *int[)]x *<< *[(]unsigned *int[)]x;$
+^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)]x *- *DANGER_CONSTANT_2u;$
+^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[\(]unsigned *int[\)]x;$
+^.*__CPROVER_danger_S0_x_0 *= *[\(]unsigned *int[\)]x *<< *[\(]unsigned *int[\)]x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_unit_full2/test.desc b/regression/cegis/cegis_danger_unit_full2/test.desc
index 54b35341472..043b25c8d05 100644
--- a/regression/cegis/cegis_danger_unit_full2/test.desc
+++ b/regression/cegis/cegis_danger_unit_full2/test.desc
@@ -3,11 +3,11 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_tmp_0 *= *[(]unsigned *int[)][(][(]unsigned *int[)]x *<= *DANGER_CONSTANT_2u *&& *DANGER_CONSTANT_2u *<= *[(]unsigned *int[)]x[)];$
-^.*__CPROVER_danger_D0_x *= *DANGER_CONSTANT_4294967295u *[+] *__CPROVER_danger_tmp_0;$
-^.*__CPROVER_danger_tmp_0 *= *[(]unsigned *int[)][(][(]signed *int[)]DANGER_CONSTANT_4294967295u *>> *[(]unsigned *int[)]x[)];$
-^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[(]unsigned *int[)]x;$
-^.*__CPROVER_danger_S0_x_0 *= *[(]unsigned *int[)]x *<< *[(]unsigned *int[)]x;$
-^.*__CPROVER_danger_S0_x_1 *= *[(]unsigned *int[)][(]__CPROVER_danger_S0_x_0 *< *DANGER_CONSTANT_0u *&& *DANGER_CONSTANT_0u *< *DANGER_CONSTANT_4294967294u[)];$
+^.*__CPROVER_danger_tmp_0 *= *[\(]unsigned *int[\)][\(][\(]unsigned *int[\)]x *<= *DANGER_CONSTANT_2u *&& *DANGER_CONSTANT_2u *<= *[\(]unsigned *int[\)]x[\)];$
+^.*__CPROVER_danger_D0_x *= *DANGER_CONSTANT_4294967295u *[\+] *__CPROVER_danger_tmp_0;$
+^.*__CPROVER_danger_tmp_0 *= *[\(]unsigned *int[\)][\(][\(]signed *int[\)]DANGER_CONSTANT_4294967295u *>> *[\(]unsigned *int[\)]x[\)];$
+^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *- *[\(]unsigned *int[\)]x;$
+^.*__CPROVER_danger_S0_x_0 *= *[\(]unsigned *int[\)]x *<< *[\(]unsigned *int[\)]x;$
+^.*__CPROVER_danger_S0_x_1 *= *[\(]unsigned *int[\)][\(]__CPROVER_danger_S0_x_0 *< *DANGER_CONSTANT_0u *&& *DANGER_CONSTANT_0u *< *DANGER_CONSTANT_4294967294u[\)];$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_unit_no_ranking/test.desc b/regression/cegis/cegis_danger_unit_no_ranking/test.desc
index 10479cc9d39..ad6c659ec3c 100644
--- a/regression/cegis/cegis_danger_unit_no_ranking/test.desc
+++ b/regression/cegis/cegis_danger_unit_no_ranking/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic --danger-no-ranking
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_unit_ranking_and_x0/test.desc b/regression/cegis/cegis_danger_unit_ranking_and_x0/test.desc
index 1ede2b9dd9d..cae82d5046b 100644
--- a/regression/cegis/cegis_danger_unit_ranking_and_x0/test.desc
+++ b/regression/cegis/cegis_danger_unit_ranking_and_x0/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)][(][(]signed *int[)]DANGER_CONSTANT_4u *>> *[(]unsigned *int[)]x[)];$
-^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *>> *[(]unsigned *int[)]x;
+^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)][\(][\(]signed *int[\)]DANGER_CONSTANT_4u *>> *[\(]unsigned *int[\)]x[\)];$
+^.*__CPROVER_danger_R0_x_0 *= *DANGER_CONSTANT_3u *>> *[\(]unsigned *int[\)]x;
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_danger_unit_x0_only/test.desc b/regression/cegis/cegis_danger_unit_x0_only/test.desc
index 02b836b17c6..1a387823ad1 100644
--- a/regression/cegis/cegis_danger_unit_x0_only/test.desc
+++ b/regression/cegis/cegis_danger_unit_x0_only/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --danger --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)][(][(]unsigned *int[)]x *<= *[(]unsigned *int[)]x *&& *[(]unsigned *int[)]x *<= *DANGER_CONSTANT_3u[)];$
-^.*__CPROVER_danger_R0_x_0 *= *~[(][(]unsigned *int[)]x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)][\(][\(]unsigned *int[\)]x *<= *[\(]unsigned *int[\)]x *&& *[\(]unsigned *int[\)]x *<= *DANGER_CONSTANT_3u[\)];$
+^.*__CPROVER_danger_R0_x_0 *= *~[\(][\(]unsigned *int[\)]x[\)];$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_00/test.desc b/regression/cegis/cegis_jsa_benchmark_00/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_00/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_00/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_01/test.desc b/regression/cegis/cegis_jsa_benchmark_01/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_01/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_01/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_02/test.desc b/regression/cegis/cegis_jsa_benchmark_02/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_02/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_02/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_03/test.desc b/regression/cegis/cegis_jsa_benchmark_03/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_03/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_03/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_04/test.desc b/regression/cegis/cegis_jsa_benchmark_04/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_04/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_04/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_05/test.desc b/regression/cegis/cegis_jsa_benchmark_05/test.desc
index 52a05c4c1ba..d3350b330e6 100644
--- a/regression/cegis/cegis_jsa_benchmark_05/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_05/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa --jsa-aggregate=max -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_06/test.desc b/regression/cegis/cegis_jsa_benchmark_06/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_06/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_06/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_07/test.desc b/regression/cegis/cegis_jsa_benchmark_07/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_07/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_07/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_08/test.desc b/regression/cegis/cegis_jsa_benchmark_08/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_08/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_08/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_09/test.desc b/regression/cegis/cegis_jsa_benchmark_09/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_09/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_09/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_10/test.desc b/regression/cegis/cegis_jsa_benchmark_10/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_10/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_10/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_11/test.desc b/regression/cegis/cegis_jsa_benchmark_11/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_11/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_11/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_12/test.desc b/regression/cegis/cegis_jsa_benchmark_12/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_12/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_12/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_13/test.desc b/regression/cegis/cegis_jsa_benchmark_13/test.desc
index c58556f9d0b..88f037ea975 100644
--- a/regression/cegis/cegis_jsa_benchmark_13/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_13/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa --jsa-aggregate=min -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_14/test.desc b/regression/cegis/cegis_jsa_benchmark_14/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_14/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_14/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_15/test.desc b/regression/cegis/cegis_jsa_benchmark_15/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_15/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_15/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_16/test.desc b/regression/cegis/cegis_jsa_benchmark_16/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_16/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_16/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_17/test.desc b/regression/cegis/cegis_jsa_benchmark_17/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_17/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_17/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_18/test.desc b/regression/cegis/cegis_jsa_benchmark_18/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_18/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_18/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_18_02/test.desc b/regression/cegis/cegis_jsa_benchmark_18_02/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_18_02/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_18_02/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_19/test.desc b/regression/cegis/cegis_jsa_benchmark_19/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_19/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_19/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_20/test.desc b/regression/cegis/cegis_jsa_benchmark_20/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_20/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_20/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_21/test.desc b/regression/cegis/cegis_jsa_benchmark_21/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_21/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_21/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_22/test.desc b/regression/cegis/cegis_jsa_benchmark_22/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_22/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_22/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_23/test.desc b/regression/cegis/cegis_jsa_benchmark_23/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_23/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_23/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_24/test.desc b/regression/cegis/cegis_jsa_benchmark_24/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_24/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_24/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_25/test.desc b/regression/cegis/cegis_jsa_benchmark_25/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_25/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_25/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_26/test.desc b/regression/cegis/cegis_jsa_benchmark_26/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_26/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_26/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_27/test.desc b/regression/cegis/cegis_jsa_benchmark_27/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_27/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_27/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_28/test.desc b/regression/cegis/cegis_jsa_benchmark_28/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_28/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_28/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_29/test.desc b/regression/cegis/cegis_jsa_benchmark_29/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_29/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_29/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_30/test.desc b/regression/cegis/cegis_jsa_benchmark_30/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_30/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_30/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_31/test.desc b/regression/cegis/cegis_jsa_benchmark_31/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_31/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_31/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_32/test.desc b/regression/cegis/cegis_jsa_benchmark_32/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_32/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_32/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_33/test.desc b/regression/cegis/cegis_jsa_benchmark_33/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_33/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_33/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_34/test.desc b/regression/cegis/cegis_jsa_benchmark_34/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_34/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_34/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_35/test.desc b/regression/cegis/cegis_jsa_benchmark_35/test.desc
index 10e9fbb1886..7af97cec36a 100644
--- a/regression/cegis/cegis_jsa_benchmark_35/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_35/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic --cegis-jsa-generate
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_36/test.desc b/regression/cegis/cegis_jsa_benchmark_36/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_36/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_36/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_37/test.desc b/regression/cegis/cegis_jsa_benchmark_37/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_37/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_37/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_38/test.desc b/regression/cegis/cegis_jsa_benchmark_38/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_38/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_38/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_39/test.desc b/regression/cegis/cegis_jsa_benchmark_39/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_39/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_39/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_40/test.desc b/regression/cegis/cegis_jsa_benchmark_40/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_40/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_40/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_41/test.desc b/regression/cegis/cegis_jsa_benchmark_41/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_41/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_41/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_42/test.desc b/regression/cegis/cegis_jsa_benchmark_42/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_42/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_42/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_43/test.desc b/regression/cegis/cegis_jsa_benchmark_43/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_43/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_43/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_44/test.desc b/regression/cegis/cegis_jsa_benchmark_44/test.desc
index 10e9fbb1886..7af97cec36a 100644
--- a/regression/cegis/cegis_jsa_benchmark_44/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_44/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic --cegis-jsa-generate
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_45/test.desc b/regression/cegis/cegis_jsa_benchmark_45/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_45/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_45/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_46/test.desc b/regression/cegis/cegis_jsa_benchmark_46/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_46/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_46/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_47/test.desc b/regression/cegis/cegis_jsa_benchmark_47/test.desc
index 02334169c67..c3924d3001c 100644
--- a/regression/cegis/cegis_jsa_benchmark_47/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_47/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic --cegis-aggregate
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_benchmark_48/test.desc b/regression/cegis/cegis_jsa_benchmark_48/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_benchmark_48/test.desc
+++ b/regression/cegis/cegis_jsa_benchmark_48/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_filter_01/test.desc b/regression/cegis/cegis_jsa_filter_01/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_filter_01/test.desc
+++ b/regression/cegis/cegis_jsa_filter_01/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_jsa_map_01/test.desc b/regression/cegis/cegis_jsa_map_01/test.desc
index fc0fa8eb921..07d2c6c73d6 100644
--- a/regression/cegis/cegis_jsa_map_01/test.desc
+++ b/regression/cegis/cegis_jsa_map_01/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --jsa -D __CPROVER --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]signed *int[)][(]MINUS_ONE *< *x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]signed *int[\)][\(]MINUS_ONE *< *x[\)];$
 ^.*__CPROVER_danger_R0_x_0 *= *ONE *- *x;$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_safety_unit_greater_two/test.desc b/regression/cegis/cegis_safety_unit_greater_two/test.desc
index 047ce9e161e..ba5ab1f42ec 100644
--- a/regression/cegis/cegis_safety_unit_greater_two/test.desc
+++ b/regression/cegis/cegis_safety_unit_greater_two/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)][(][(]unsigned *int[)]x *<= *[(]unsigned *int[)]x *&& *[(]unsigned *int[)]x *<= *DANGER_CONSTANT_3u[)];$
-^.*__CPROVER_danger_R0_x_0 *= *~[(][(]unsigned *int[)]x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)][\(][\(]unsigned *int[\)]x *<= *[\(]unsigned *int[\)]x *&& *[\(]unsigned *int[\)]x *<= *DANGER_CONSTANT_3u[\)];$
+^.*__CPROVER_danger_R0_x_0 *= *~[\(][\(]unsigned *int[\)]x[\)];$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_safety_unit_true/test.desc b/regression/cegis/cegis_safety_unit_true/test.desc
index f3f8fe146b0..60aab0a2cea 100644
--- a/regression/cegis/cegis_safety_unit_true/test.desc
+++ b/regression/cegis/cegis_safety_unit_true/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)][(][(]unsigned *int[)]x *<= *[(]unsigned *int[)]x *&& *[(]unsigned *int[)]x *<= *DANGER_CONSTANT_3u[)];$
-^.*__CPROVER_danger_R0_x_0 *= *~[(][(]unsigned *int[)]x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)][\(][\(]unsigned *int[\)]x *<= *[\(]unsigned *int[\)]x *&& *[\(]unsigned *int[\)]x *<= *DANGER_CONSTANT_3u[\)];$
+^.*__CPROVER_danger_R0_x_0 *= *~[\(][\(]unsigned *int[\)]x[\)];$
 --
 ^warning: ignoring
diff --git a/regression/cegis/cegis_safety_unit_true2/test.desc b/regression/cegis/cegis_safety_unit_true2/test.desc
index 047ce9e161e..ba5ab1f42ec 100644
--- a/regression/cegis/cegis_safety_unit_true2/test.desc
+++ b/regression/cegis/cegis_safety_unit_true2/test.desc
@@ -3,7 +3,7 @@ main.c
 --gcc --safety --cegis-statistics --cegis-genetic
 ^EXIT=0$
 ^SIGNAL=0$
-^.*__CPROVER_danger_D0_x *= *[(]unsigned *int[)][(][(]unsigned *int[)]x *<= *[(]unsigned *int[)]x *&& *[(]unsigned *int[)]x *<= *DANGER_CONSTANT_3u[)];$
-^.*__CPROVER_danger_R0_x_0 *= *~[(][(]unsigned *int[)]x[)];$
+^.*__CPROVER_danger_D0_x *= *[\(]unsigned *int[\)][\(][\(]unsigned *int[\)]x *<= *[\(]unsigned *int[\)]x *&& *[\(]unsigned *int[\)]x *<= *DANGER_CONSTANT_3u[\)];$
+^.*__CPROVER_danger_R0_x_0 *= *~[\(][\(]unsigned *int[\)]x[\)];$
 --
 ^warning: ignoring
diff --git a/regression/cpp-linter/throw/test.desc b/regression/cpp-linter/throw/test.desc
index ebd3926785e..3162178e4e1 100644
--- a/regression/cpp-linter/throw/test.desc
+++ b/regression/cpp-linter/throw/test.desc
@@ -2,7 +2,7 @@ CORE
 main.cpp
 
 main\.cpp:25:  Do not include brackets when throwing an error  \[readability/throw\] \[4\]
-main\.cpp:26:  Extra space before ( in function call  \[whitespace/parens\] \[4\]
+main\.cpp:26:  Extra space before \( in function call  \[whitespace/parens\] \[4\]
 main\.cpp:26:  Do not include brackets when throwing an error  \[readability/throw\] \[4\]
 main\.cpp:28:  First character of throw error message should be lower case  \[readability/throw\] \[4\]
 main\.cpp:29:  Do not include brackets when throwing an error  \[readability/throw\] \[4\]
diff --git a/regression/cpp/Address_of_Method2/test.desc b/regression/cpp/Address_of_Method2/test.desc
index 1f21d7d0c49..bd3820cce3a 100644
--- a/regression/cpp/Address_of_Method2/test.desc
+++ b/regression/cpp/Address_of_Method2/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.cpp
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --
diff --git a/regression/cpp/Address_of_Method3/test.desc b/regression/cpp/Address_of_Method3/test.desc
index 1f21d7d0c49..bd3820cce3a 100644
--- a/regression/cpp/Address_of_Method3/test.desc
+++ b/regression/cpp/Address_of_Method3/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.cpp
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --
diff --git a/regression/cpp/Constant2/test.desc b/regression/cpp/Constant2/test.desc
index 1aaf62c1e14..166ae78593b 100644
--- a/regression/cpp/Constant2/test.desc
+++ b/regression/cpp/Constant2/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.cpp
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --
diff --git a/regression/cpp/Constant3/test.desc b/regression/cpp/Constant3/test.desc
index 1aaf62c1e14..166ae78593b 100644
--- a/regression/cpp/Constant3/test.desc
+++ b/regression/cpp/Constant3/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.cpp
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --
diff --git a/regression/cpp/Pointer_Conversion1/test.desc b/regression/cpp/Pointer_Conversion1/test.desc
index 1f21d7d0c49..bd3820cce3a 100644
--- a/regression/cpp/Pointer_Conversion1/test.desc
+++ b/regression/cpp/Pointer_Conversion1/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.cpp
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --
diff --git a/regression/cpp/Resolver12/test.desc b/regression/cpp/Resolver12/test.desc
index 1f21d7d0c49..bd3820cce3a 100644
--- a/regression/cpp/Resolver12/test.desc
+++ b/regression/cpp/Resolver12/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.cpp
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --
diff --git a/regression/cpp/Resolver4/test.desc b/regression/cpp/Resolver4/test.desc
index 1f21d7d0c49..bd3820cce3a 100644
--- a/regression/cpp/Resolver4/test.desc
+++ b/regression/cpp/Resolver4/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.cpp
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --
diff --git a/regression/cpp/union3/test.desc b/regression/cpp/union3/test.desc
index 1f21d7d0c49..bd3820cce3a 100644
--- a/regression/cpp/union3/test.desc
+++ b/regression/cpp/union3/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.cpp
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --
diff --git a/regression/cpp/union4/test.desc b/regression/cpp/union4/test.desc
index 1f21d7d0c49..bd3820cce3a 100644
--- a/regression/cpp/union4/test.desc
+++ b/regression/cpp/union4/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.cpp
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --
diff --git a/regression/cpp/union5/test.desc b/regression/cpp/union5/test.desc
index 1f21d7d0c49..bd3820cce3a 100644
--- a/regression/cpp/union5/test.desc
+++ b/regression/cpp/union5/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.cpp
 
-^EXIT=\(64\|1\)$
+^EXIT=(64|1)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
 --
diff --git a/regression/goto-instrument/data-flow1/test.desc b/regression/goto-instrument/data-flow1/test.desc
index a11f4754f21..eb4fc8394e4 100644
--- a/regression/goto-instrument/data-flow1/test.desc
+++ b/regression/goto-instrument/data-flow1/test.desc
@@ -3,6 +3,6 @@ main.c
 --show-dependence-graph
 ^EXIT=0$
 ^SIGNAL=0$
-Data dependencies: *[0-9]\+,[0-9]\+,[0-9]\+
+Data dependencies: *[0-9]+,[0-9]+,[0-9]+
 --
 ^warning: ignoring
diff --git a/regression/goto-instrument/inline_01/test.desc b/regression/goto-instrument/inline_01/test.desc
index 36bbb89719e..85d55daa118 100644
--- a/regression/goto-instrument/inline_01/test.desc
+++ b/regression/goto-instrument/inline_01/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
-f[(].*[)];$
-g[(].*[)];$
-h[(].*[)];$
+f[\(].*[\)];$
+g[\(].*[\)];$
+h[\(].*[\)];$
 ^warning: ignoring
diff --git a/regression/goto-instrument/inline_02/test.desc b/regression/goto-instrument/inline_02/test.desc
index ee604db74c9..20e93e09f77 100644
--- a/regression/goto-instrument/inline_02/test.desc
+++ b/regression/goto-instrument/inline_02/test.desc
@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-f[(].*[)];$
-g[(].*[)];$
-h[(].*[)];$
+f[\(].*[\)];$
+g[\(].*[\)];$
+h[\(].*[\)];$
 --
 ^warning: ignoring
diff --git a/regression/goto-instrument/inline_03/test.desc b/regression/goto-instrument/inline_03/test.desc
index 4681dd60cea..3b6645c8a4c 100644
--- a/regression/goto-instrument/inline_03/test.desc
+++ b/regression/goto-instrument/inline_03/test.desc
@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-f[(].*[)];$
-g[(].*[)];$
+f[\(].*[\)];$
+g[\(].*[\)];$
 --
-h[(].*[)];$
+h[\(].*[\)];$
 ^warning: ignoring
diff --git a/regression/goto-instrument/inline_04/test.desc b/regression/goto-instrument/inline_04/test.desc
index b4f0cef0dfa..8f2f03cf5f3 100644
--- a/regression/goto-instrument/inline_04/test.desc
+++ b/regression/goto-instrument/inline_04/test.desc
@@ -4,9 +4,9 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-g[(].*[)];$
-h[(].*[)];$
+g[\(].*[\)];$
+h[\(].*[\)];$
 --
-f[(].*[)];$
-other_func[(].*[)];$
+f[\(].*[\)];$
+other_func[\(].*[\)];$
 ^warning: ignoring
diff --git a/regression/goto-instrument/inline_11/test.desc b/regression/goto-instrument/inline_11/test.desc
index 562879b7646..ca980d9baa6 100644
--- a/regression/goto-instrument/inline_11/test.desc
+++ b/regression/goto-instrument/inline_11/test.desc
@@ -5,5 +5,5 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
-main[(].*[)];
+main[\(].*[\)];
 ^warning: ignoring
diff --git a/regression/strings/test3/test.desc b/regression/strings/test3/test.desc
index 54e56188c1b..24ed719acc2 100644
--- a/regression/strings/test3/test.desc
+++ b/regression/strings/test3/test.desc
@@ -3,8 +3,8 @@ test.c
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_string_length(s) == i + 5: SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"po\"),s): SUCCESS$
-^\[main.assertion.3\] assertion __CPROVER_char_at(s, i) == .p.: SUCCESS$
-^\[main.assertion.4\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal(\"p!o\"), s): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_length\(s\) == i \+ 5: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\(\"po\"\),s\): SUCCESS$
+^\[main.assertion.3\] assertion __CPROVER_char_at\(s, i\) == .p.: SUCCESS$
+^\[main.assertion.4\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\(\"p!o\"\), s\): FAILURE$
 --
diff --git a/regression/strings/test_char_set/test.desc b/regression/strings/test_char_set/test.desc
index 589767e4b82..99f3cfd81de 100644
--- a/regression/strings/test_char_set/test.desc
+++ b/regression/strings/test_char_set/test.desc
@@ -3,6 +3,6 @@ test.c
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("apc")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_string_equal(t, __CPROVER_string_literal("abc")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal\(t, __CPROVER_string_literal\("apc"\)): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal\(t, __CPROVER_string_literal\("abc"\)): FAILURE$
 --
diff --git a/regression/strings/test_concat/test.desc b/regression/strings/test_concat/test.desc
index c3f1ca2a65a..8df68c18bc3 100644
--- a/regression/strings/test_concat/test.desc
+++ b/regression/strings/test_concat/test.desc
@@ -4,5 +4,5 @@ test.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion c == .p.: SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_char_at(u,2) == .p.: FAILURE$
+^\[main.assertion.2\] assertion __CPROVER_char_at\(u,2\) == .p.: FAILURE$
 --
diff --git a/regression/strings/test_contains/test.desc b/regression/strings/test_contains/test.desc
index fcf9694b31d..f2414880794 100644
--- a/regression/strings/test_contains/test.desc
+++ b/regression/strings/test_contains/test.desc
@@ -3,7 +3,7 @@ test.c
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"3\")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"12\")): SUCCESS$
-^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_contains_func(t, __CPROVER_uninterpreted_string_literal_func(\"b\")): FAILURE$
+^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"3\"\)): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_uninterpreted_string_contains_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"12\"\)): SUCCESS$
+^\[main.assertion.3\] assertion !__CPROVER_uninterpreted_string_contains_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"b\"\)): FAILURE$
 --
diff --git a/regression/strings/test_equal/test.desc b/regression/strings/test_equal/test.desc
index d3cfd4f3747..5fbe05f8fdd 100644
--- a/regression/strings/test_equal/test.desc
+++ b/regression/strings/test_equal/test.desc
@@ -3,6 +3,6 @@ test.c
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("pippo")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_string_equal(s, __CPROVER_string_literal("mippo")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal\(s, __CPROVER_string_literal\("pippo"\)): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal\(s, __CPROVER_string_literal\("mippo"\)): FAILURE$
 --
diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc
index a13b3dad852..8d78e11e71b 100644
--- a/regression/strings/test_int/test.desc
+++ b/regression/strings/test_int/test.desc
@@ -3,8 +3,8 @@ test.c
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_char_at(s,0) == .1.: SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_char_at(s,1) == .2.: SUCCESS$
+^\[main.assertion.1\] assertion __CPROVER_char_at\(s,0\) == .1.: SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_char_at\(s,1\) == .2.: SUCCESS$
 ^\[main.assertion.3\] assertion j == 234: SUCCESS$
-^\[main.assertion.4\] assertion j < 233 || __CPROVER_char_at(s,2) == .4.: FAILURE$
+^\[main.assertion.4\] assertion j < 233 || __CPROVER_char_at\(s,2\) == .4.: FAILURE$
 --
diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc
index 4e7cd79fde4..9bb75eda5b6 100644
--- a/regression/strings/test_pass1/test.desc
+++ b/regression/strings/test_pass1/test.desc
@@ -3,6 +3,6 @@ test.c
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"a\")): SUCCESS
-^\[main.assertion.2\] assertion !__CPROVER_uninterpreted_string_equal_func(t, __CPROVER_uninterpreted_string_literal_func(\"a\")): FAILURE$
-^\*\* 1 of 2 failed (2 iterations)$
+^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): SUCCESS
+^\[main.assertion.2\] assertion !__CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): FAILURE$
+^\*\* 1 of 2 failed \(2 iterations\)$
diff --git a/regression/strings/test_pass_pc3/test.desc b/regression/strings/test_pass_pc3/test.desc
index 0e64d9b84d1..3edb9f68f7a 100644
--- a/regression/strings/test_pass_pc3/test.desc
+++ b/regression/strings/test_pass_pc3/test.desc
@@ -3,6 +3,6 @@ test.c
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_string_length(s3) == 0: FAILURE$
-^\[main.assertion.2\] assertion __CPROVER_string_length(s3) < 2: SUCCESS$
+^\[main.assertion.1\] assertion __CPROVER_string_length\(s3\) == 0: FAILURE$
+^\[main.assertion.2\] assertion __CPROVER_string_length\(s3\) < 2: SUCCESS$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/test_substring/test.desc b/regression/strings/test_substring/test.desc
index 6e2609d9cd3..a32376aca23 100644
--- a/regression/strings/test_substring/test.desc
+++ b/regression/strings/test_substring/test.desc
@@ -3,8 +3,8 @@ test.c
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cd")): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_string_equal(t,__CPROVER_string_literal("cc")): FAILURE$
-^\[main.assertion.3\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("bc")): SUCCESS$
-^\[main.assertion.4\] assertion !__CPROVER_string_equal(t,__CPROVER_string_literal("cd")): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_equal\(t,__CPROVER_string_literal\("cd"\)): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_equal\(t,__CPROVER_string_literal\("cc"\)): FAILURE$
+^\[main.assertion.3\] assertion !__CPROVER_string_equal\(t,__CPROVER_string_literal\("bc"\)): SUCCESS$
+^\[main.assertion.4\] assertion !__CPROVER_string_equal\(t,__CPROVER_string_literal\("cd"\)): FAILURE$
 --
diff --git a/regression/strings/test_suffix/test.desc b/regression/strings/test_suffix/test.desc
index a6667cfbfcf..9f425595434 100644
--- a/regression/strings/test_suffix/test.desc
+++ b/regression/strings/test_suffix/test.desc
@@ -3,6 +3,6 @@ test.c
 --string-refine
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.1\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("po"),s): SUCCESS$
-^\[main.assertion.2\] assertion __CPROVER_string_issuffix(__CPROVER_string_literal("pp"),s): FAILURE$
+^\[main.assertion.1\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\("po"\),s\): SUCCESS$
+^\[main.assertion.2\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\("pp"\),s\): FAILURE$
 --
diff --git a/regression/taint/aliasing1/test.desc b/regression/taint/aliasing1/test.desc
index f2f765d40b6..a0ac6401d67 100644
--- a/regression/taint/aliasing1/test.desc
+++ b/regression/taint/aliasing1/test.desc
@@ -3,7 +3,7 @@ aliasing1.class
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$
-^file aliasing1.java line 10: There is a flow (taint rule my_sink)$
+^file aliasing1.java line 10: There is a flow \(taint rule my_sink\)$
 --
-^file aliasing1.java line 8: There is a flow (taint rule my_sink)$
+^file aliasing1.java line 8: There is a flow \(taint rule my_sink\)$
 ^warning: ignoring
diff --git a/regression/taint/basic1/test.desc b/regression/taint/basic1/test.desc
index d96a4d0c427..c4384ac9655 100644
--- a/regression/taint/basic1/test.desc
+++ b/regression/taint/basic1/test.desc
@@ -3,7 +3,7 @@ basic1.class
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$
-^file basic1.java line 8: There is a T1 flow (taint rule my_h1)$
-^file basic1.java line 11: There is a T2 flow (taint rule my_h2)$
+^file basic1.java line 8: There is a T1 flow \(taint rule my_h1\)$
+^file basic1.java line 11: There is a T2 flow \(taint rule my_h2\)$
 --
 ^warning: ignoring
diff --git a/regression/taint/basic2/test.desc b/regression/taint/basic2/test.desc
index 25d5141cfa5..428281280c8 100644
--- a/regression/taint/basic2/test.desc
+++ b/regression/taint/basic2/test.desc
@@ -3,7 +3,7 @@ basic2.class
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$
-^file basic2.java line 8: There is a T1 flow (taint rule my_h1)$
-^file basic2.java line 11: There is a T2 flow (taint rule my_h2)$
+^file basic2.java line 8: There is a T1 flow \(taint rule my_h1\)$
+^file basic2.java line 11: There is a T2 flow \(taint rule my_h2\)$
 --
 ^warning: ignoring
diff --git a/regression/taint/interface1/test.desc b/regression/taint/interface1/test.desc
index d24d8b6bfc5..6ac81f15786 100644
--- a/regression/taint/interface1/test.desc
+++ b/regression/taint/interface1/test.desc
@@ -3,6 +3,6 @@ interface1.class
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$
-^file interface1.java line 18: There is a flow! (taint rule sink_rule)$
+^file interface1.java line 18: There is a flow! \(taint rule sink_rule\)$
 --
 ^warning: ignoring
diff --git a/regression/taint/map1/test.desc b/regression/taint/map1/test.desc
index 25bf4fb7e58..5526aa21b3a 100644
--- a/regression/taint/map1/test.desc
+++ b/regression/taint/map1/test.desc
@@ -3,6 +3,6 @@ map1.class
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$
-^file map1.java line 12: There is a flow (taint rule my_sink)$
+^file map1.java line 12: There is a flow \(taint rule my_sink\)$
 --
 ^warning: ignoring
diff --git a/regression/test-script/Makefile b/regression/test-script/Makefile
new file mode 100644
index 00000000000..ba7db5e6250
--- /dev/null
+++ b/regression/test-script/Makefile
@@ -0,0 +1,46 @@
+
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../program_runner.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+	@echo "Testing KNOWNBUG fail"
+
+	@if ! ../test.pl -c ../program_runner.sh -K ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+tests.log:
+	pwd
+	@if ! ../test.pl -c ../program_runner.sh ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+	@echo "Testing KNOWNBUG fail"
+
+	@if ! ../test.pl -c ../program_runner.sh -K ; then \
+		../failed-tests-printer.pl ; \
+		exit 1; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		rm -f tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			rm -f *.out *.gb; \
+			cd ..; \
+		fi \
+	done
diff --git a/regression/test-script/excluded-line/program.c b/regression/test-script/excluded-line/program.c
new file mode 100755
index 00000000000..882fedcc2fd
--- /dev/null
+++ b/regression/test-script/excluded-line/program.c
@@ -0,0 +1,7 @@
+#include <stdio.h>
+
+int main(void) {
+  printf("Hello\n");
+  printf("World\n");
+  return 0;
+}
diff --git a/regression/test-script/excluded-line/test.desc b/regression/test-script/excluded-line/test.desc
new file mode 100644
index 00000000000..2384efe0828
--- /dev/null
+++ b/regression/test-script/excluded-line/test.desc
@@ -0,0 +1,6 @@
+CORE
+program.c
+
+^Hello$
+--
+^Goodbye$
diff --git a/regression/test-script/failing-excluded-line/program.c b/regression/test-script/failing-excluded-line/program.c
new file mode 100755
index 00000000000..882fedcc2fd
--- /dev/null
+++ b/regression/test-script/failing-excluded-line/program.c
@@ -0,0 +1,7 @@
+#include <stdio.h>
+
+int main(void) {
+  printf("Hello\n");
+  printf("World\n");
+  return 0;
+}
diff --git a/regression/test-script/failing-excluded-line/test.desc b/regression/test-script/failing-excluded-line/test.desc
new file mode 100644
index 00000000000..36668db5a5f
--- /dev/null
+++ b/regression/test-script/failing-excluded-line/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+program.c
+
+^Hello$
+--
+^World$
+--
+This isn't really a known bug perse, instead this test should fail (since these
+are tests of the test runner).
diff --git a/regression/test-script/failing-multi-line/program.c b/regression/test-script/failing-multi-line/program.c
new file mode 100755
index 00000000000..882fedcc2fd
--- /dev/null
+++ b/regression/test-script/failing-multi-line/program.c
@@ -0,0 +1,7 @@
+#include <stdio.h>
+
+int main(void) {
+  printf("Hello\n");
+  printf("World\n");
+  return 0;
+}
diff --git a/regression/test-script/failing-multi-line/test.desc b/regression/test-script/failing-multi-line/test.desc
new file mode 100644
index 00000000000..cf4fcf3034b
--- /dev/null
+++ b/regression/test-script/failing-multi-line/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+program.c
+
+activate-multi-line-match
+Hello\nAnother\nWorld
+--
+--
+This isn't really a known bug perse, instead this test should fail (since these
+are tests of the test runner).
diff --git a/regression/test-script/failing-single-line/program.c b/regression/test-script/failing-single-line/program.c
new file mode 100755
index 00000000000..882fedcc2fd
--- /dev/null
+++ b/regression/test-script/failing-single-line/program.c
@@ -0,0 +1,7 @@
+#include <stdio.h>
+
+int main(void) {
+  printf("Hello\n");
+  printf("World\n");
+  return 0;
+}
diff --git a/regression/test-script/failing-single-line/test.desc b/regression/test-script/failing-single-line/test.desc
new file mode 100644
index 00000000000..604682ecbdb
--- /dev/null
+++ b/regression/test-script/failing-single-line/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+program.c
+
+^Goodbye$
+--
+--
+This isn't really a known bug perse, instead this test should fail (since these
+are tests of the test runner).
diff --git a/regression/test-script/multi-line/program.c b/regression/test-script/multi-line/program.c
new file mode 100755
index 00000000000..882fedcc2fd
--- /dev/null
+++ b/regression/test-script/multi-line/program.c
@@ -0,0 +1,7 @@
+#include <stdio.h>
+
+int main(void) {
+  printf("Hello\n");
+  printf("World\n");
+  return 0;
+}
diff --git a/regression/test-script/multi-line/test.desc b/regression/test-script/multi-line/test.desc
new file mode 100644
index 00000000000..cf9bb072880
--- /dev/null
+++ b/regression/test-script/multi-line/test.desc
@@ -0,0 +1,6 @@
+CORE
+program.c
+
+activate-multi-line-match
+Hello\nWorld
+--
diff --git a/regression/test-script/program_runner.sh b/regression/test-script/program_runner.sh
new file mode 100755
index 00000000000..8e09b75f0ab
--- /dev/null
+++ b/regression/test-script/program_runner.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+set -e
+
+gcc $1 -o a.out
+./a.out
diff --git a/regression/test-script/single-line/program.c b/regression/test-script/single-line/program.c
new file mode 100755
index 00000000000..882fedcc2fd
--- /dev/null
+++ b/regression/test-script/single-line/program.c
@@ -0,0 +1,7 @@
+#include <stdio.h>
+
+int main(void) {
+  printf("Hello\n");
+  printf("World\n");
+  return 0;
+}
diff --git a/regression/test-script/single-line/test.desc b/regression/test-script/single-line/test.desc
new file mode 100644
index 00000000000..2507fd6a412
--- /dev/null
+++ b/regression/test-script/single-line/test.desc
@@ -0,0 +1,5 @@
+CORE
+program.c
+
+^Hello$
+--
diff --git a/regression/test.pl b/regression/test.pl
index 066fe2a572f..a2ac088d0e0 100755
--- a/regression/test.pl
+++ b/regression/test.pl
@@ -4,6 +4,8 @@
 use strict;
 use warnings;
 
+use Cwd;
+
 my $has_thread_pool = eval
 {
   # "http://www.cpan.org/authors/id/J/JW/JWU/Thread-Pool-Simple/Thread-Pool-Simple-0.25.tar.gz"
@@ -61,13 +63,9 @@ ($$$$$)
   my ($name, $test, $t_level, $cmd, $ign) = @_;
   my ($level, $input, $options, $grep_options, @results) = load("$test");
 
-  # If the 4th line starts with a '-' we use that line as options to pass to
-  # grep when matching all lines in this test
-  if($grep_options =~ /^-/) {
-    print "\nActivating perl flags: $grep_options\n";
-  }
-  else {
-    # No grep options so stick this back into the results array
+  # If the 4th line is activate-multi-line-match we enable multi-line checks
+  if($grep_options ne "activate-multi-line-match") {
+    # No such flag, so we add it back in
     unshift @results, $grep_options;
     $grep_options = "";
   }
@@ -117,10 +115,43 @@ ($$$$$)
           $included--;
         } else {
           my $r;
-          $result =~ s/\\/\\\\/g;
-          $result =~ s/([^\\])\$/$1\\r\\\\?\$/;
-          system("bash", "-c", "grep $grep_options \$'$result' '$name/$output' >/dev/null");
-          $r = ($included ? $? != 0 : $? == 0);
+
+          my $dir = getcwd();
+          my $abs_path = "$dir/$name/$output";
+          open(my $fh => $abs_path) || die "Cannot open '$name/$output': $!";
+
+          # Multi line therefore we run each check across the whole output
+          if($grep_options eq "activate-multi-line-match") {
+            local $/ = undef;
+            binmode $fh;
+            my $whole_file = <$fh>;
+            my $is_match = $whole_file =~ /$result/;
+            $r = ($included ? !$is_match : $is_match);
+          }
+          else
+          {
+            my $found_line = 0;
+            while(my $line = <$fh>) {
+              if($line =~ /$result/) {
+                # We've found the line, therefore if it is included we set
+                # the result to 0 (OK) If it is excluded, we set the result
+                # to 1 (FAILED)
+                $r = !$included;
+                $found_line = 1;
+                last;
+              }
+            }
+
+            if($found_line == 0) {
+              # None of the lines matched, therefore the result is set to
+              # 0 (OK) if and only if the line was not meant to be included
+              $r = $included;
+            }
+
+          }
+          close($fh);
+
+
           if($r) {
             print LOG "$result [FAILED]\n";
             $failed = 1;
@@ -134,11 +165,15 @@ ($$$$$)
     }
   } else {
     print LOG "Execution [SKIPPED]\n";
+    return 2;
   }
 
   print LOG "\n";
 
-  return $failed;
+  # if the test is a KNOWNBUG then the test should fail
+  my $should_fail = $level eq 8;
+
+  return ($should_fail != $failed);
 }
 
 sub dirs() {
@@ -185,7 +220,7 @@ ($$$$)
 <level>
 <main source>
 <options>
-<grep_options>
+<activate-multi-line-match>
 <required patterns>
 --
 <disallowed patterns>
@@ -193,16 +228,15 @@ ($$$$)
 <comment text>
 
 where
-  <level>                is one of CORE, THOROUGH, FUTURE or KNOWNBUG
-  <main source>          is a file with extension .c/.i/.gb/.cpp/.ii/.xml/.class/.jar
-  <options>              additional options to be passed to CMD
-  <grep_options>         additional flags to be passed to grep when checking required
-                         patterns (this is optional, if the line stats with a `-'
-                         it will be used as grep options. Otherwise, it will be
-                         considered part of the required patterns)
-  <required patterns>    one or more lines of regualar expressions that must occur in the output
-  <disallowed patterns>  one or more lines of expressions that must not occur in output
-  <comment text>         free form text
+  <level>                         is one of CORE, THOROUGH, FUTURE or KNOWNBUG
+  <main source>                   is a file with extension .c/.i/.gb/.cpp/.ii/.xml/.class/.jar
+  <options>                       additional options to be passed to CMD
+  <activate-multi-line-match>     The fourth line can optionally be activate-multi-line-match, if this is the
+                                  case then each of the rules will be matched over multiple lines (so can contain)
+                                  the new line symbol (\\n) inside them.
+  <required patterns>             one or more lines of regualar expressions that must occur in the output
+  <disallowed patterns>           one or more lines of expressions that must not occur in output
+  <comment text>                  free form text
 
 EOF
   exit 1;