diff --git a/jbmc/regression/janalyzer/string-initializer/test.desc b/jbmc/regression/janalyzer/string-initializer/test.desc
index affa856055e..67e49735084 100644
--- a/jbmc/regression/janalyzer/string-initializer/test.desc
+++ b/jbmc/regression/janalyzer/string-initializer/test.desc
@@ -3,7 +3,7 @@ Basic1
 --location-sensitive --constants --show
 ^EXIT=0$
 ^SIGNAL=0$
-Hello_20 = \{ \.@class_identifier="java::java\.lang\.String" \};
+Hello_20 := \{ "java::java\.lang\.String" \}
 java::java\.lang\.String\.Literal\.Hello_20=\{ \.@class_identifier="java::java\.lang\.String" \}
 --
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/JumpSimplification/test.desc b/jbmc/regression/jbmc/JumpSimplification/test.desc
index b98eb8839f6..72de52a240b 100644
--- a/jbmc/regression/jbmc/JumpSimplification/test.desc
+++ b/jbmc/regression/jbmc/JumpSimplification/test.desc
@@ -4,7 +4,7 @@ Test
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-IF \w* <= 0 THEN GOTO 1\n\s*//.*\n\s*//.*\n\s*\w*::
+IF .* ≤ 0 THEN GOTO 1\n\s*//.*\n\s*//.*\n\s*ASSIGN
 --
-IF !\(\w* <= 0\) THEN GOTO 1\n\s*//.*\n.*GOTO 2\n\s*//.*\n\s*//.*\n\s*1: \w*::
+IF ¬\(.* ≤ 0\) THEN GOTO 1\n\s*//.*\n.*GOTO 2\n\s*//.*\n\s*//.*\n\s*1: \w*::
 ^warning: ignoring
diff --git a/jbmc/regression/jbmc/LocalVarTable5/test.desc b/jbmc/regression/jbmc/LocalVarTable5/test.desc
index 46562fc0cf6..83038f5b177 100644
--- a/jbmc/regression/jbmc/LocalVarTable5/test.desc
+++ b/jbmc/regression/jbmc/LocalVarTable5/test.desc
@@ -1,10 +1,10 @@
 CORE
 test
 --show-goto-functions --function test.main
-dead anonlocal::1i
-dead anonlocal::2i
-dead anonlocal::3a
-dead new_tmp[0-9]+
+DEAD .*::anonlocal::1i
+DEAD .*::anonlocal::2i
+DEAD .*::anonlocal::3a
+DEAD .*::new_tmp[0-9]+
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc b/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc
index 93216e04753..f9d8e26f17a 100644
--- a/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc
+++ b/jbmc/regression/jbmc/clinit-lifting2/test-goto-functions.desc
@@ -4,7 +4,7 @@ Test
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\s*// 0 no location\n\s*Other\.<clinit_wrapper>\(\);\s*// 1 no location\s*int total;
+\s*// 0 no location\n\s*CALL java::Other\.<clinit_wrapper>\(\)\s*// 1 no location\s*DECL .*::total
 --
 --
 This checks that the clinit-wrapper function is called once, even though there are two calls in the source
diff --git a/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc b/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc
index 3397098c5f3..f3c4410882b 100644
--- a/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc
+++ b/jbmc/regression/jbmc/clinit-lifting3/test-goto-functions.desc
@@ -4,7 +4,7 @@ Test
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\s*// 0 no location\n\s*Other\.<clinit_wrapper>\(\);\s*// 1 no location\s*Third\.<clinit_wrapper>\(\);\s*// 2 no location\s*int total;
+\s*// 0 no location\n\s*CALL java::Other\.<clinit_wrapper>\(\)\s*// 1 no location\s*CALL java::Third\.<clinit_wrapper>\(\)\s*// 2 no location\s*DECL .*::total
 --
 --
 This checks that the clinit-wrapper function is called once, even though there are two calls in the source
diff --git a/jbmc/regression/jbmc/destructor1/test.desc b/jbmc/regression/jbmc/destructor1/test.desc
index 350d4266507..f201cfae114 100644
--- a/jbmc/regression/jbmc/destructor1/test.desc
+++ b/jbmc/regression/jbmc/destructor1/test.desc
@@ -3,6 +3,6 @@ Break
 --show-goto-functions --function Break.main
 ^EXIT=0$
 ^SIGNAL=0$
-dead i;
+DEAD .*::i
 --
 GOTO 11
diff --git a/jbmc/regression/jbmc/destructors/block.desc b/jbmc/regression/jbmc/destructors/block.desc
index 0e919c84a98..dbf5a2bb539 100644
--- a/jbmc/regression/jbmc/destructors/block.desc
+++ b/jbmc/regression/jbmc/destructors/block.desc
@@ -2,7 +2,7 @@ CORE
 DestructorStackTests
 --show-goto-functions --function DestructorStackTests.mainTest --unwind 10
 activate-multi-line-match
-[0-9]+: dead strings;[\s]*(?P<comment_block>(\/\/ [0-9]+ file DestructorStackTests\.java line 42 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 90)|(\/\/ [0-9]+ no location))[\s]*dead minor1;[\s]*(?P>comment_block)[\s]*dead anonlocal::[0-9a-zA-Z]+;[\s]*(?P>comment_block)[\s]*[0-9]+: END_FUNCTION
+[0-9]+: DEAD .*::strings[\s]*(?P<comment_block>(\/\/ [0-9]+ file DestructorStackTests\.java line 42 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 90)|(\/\/ [0-9]+ no location))[\s]*DEAD .*::minor1[\s]*(?P>comment_block)[\s]*DEAD .*::anonlocal::[0-9a-zA-Z]+[\s]*(?P>comment_block)[\s]*[0-9]+: END_FUNCTION
 ^EXIT=0$
 ^SIGNAL=0$
 --
@@ -10,11 +10,11 @@ activate-multi-line-match
 Checks for:
 
            // Labels: pc187
-       12: dead strings;
+       12: DEAD strings
            // 250 file DestructorStackTests.java line 42 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 90
-           dead minor1;
+           DEAD minor1
            // 251 file DestructorStackTests.java line 42 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 90
-           dead anonlocal::4a;
+           DEAD anonlocal::4a
            // 252 no location
        13: END_FUNCTION
 
diff --git a/jbmc/regression/jbmc/destructors/break.desc b/jbmc/regression/jbmc/destructors/break.desc
index 165fc5fe184..6cf469b6b8c 100644
--- a/jbmc/regression/jbmc/destructors/break.desc
+++ b/jbmc/regression/jbmc/destructors/break.desc
@@ -2,7 +2,7 @@ CORE
 DestructorStackTests
 --show-goto-functions --function DestructorStackTests.mainTest --unwind 10
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 34 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 84)[\s]*dead throwaway;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead val;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
+(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 34 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 84)[\s]*DEAD .*::throwaway[\s]*(?P>comment_block)[\s]*DEAD .*::new_tmp[0-9]+[\s]*(?P>comment_block)[\s]*DEAD .*::val[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
 ^EXIT=0$
 ^SIGNAL=0$
 --
@@ -10,11 +10,11 @@ activate-multi-line-match
 Checks for:
 
         // 228 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
-        dead throwaway;
+        DEAD throwaway
         // 229 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
-        dead new_tmp16;
+        DEAD new_tmp16
         // 230 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
-        dead val;
+        DEAD val
         // 231 file DestructorStackTests.java line 34 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 84
         GOTO 12
 
diff --git a/jbmc/regression/jbmc/destructors/continue.desc b/jbmc/regression/jbmc/destructors/continue.desc
index 5f9815db194..1aaef528f31 100644
--- a/jbmc/regression/jbmc/destructors/continue.desc
+++ b/jbmc/regression/jbmc/destructors/continue.desc
@@ -2,7 +2,7 @@ CORE
 DestructorStackTests
 --show-goto-functions --function DestructorStackTests.mainTest --unwind 10
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 39 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 89)[\s]*dead throwaway;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead val;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
+(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 39 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 89)[\s]*DEAD .*::throwaway[\s]*(?P>comment_block)[\s]*DEAD .*::new_tmp[0-9]+[\s]*(?P>comment_block)[\s]*DEAD .*::val[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
 ^EXIT=0$
 ^SIGNAL=0$
 --
@@ -10,11 +10,11 @@ activate-multi-line-match
 Checks for:
 
         // 242 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
-        dead throwaway;
+        DEAD throwaway
         // 243 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
-        dead new_tmp17;
+        DEAD new_tmp17
         // 244 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
-        dead val;
+        DEAD val
         // 245 file DestructorStackTests.java line 39 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 89
         GOTO 3
 
diff --git a/jbmc/regression/jbmc/destructors/decl.desc b/jbmc/regression/jbmc/destructors/decl.desc
index 496f40a795f..a4ce1207ffa 100644
--- a/jbmc/regression/jbmc/destructors/decl.desc
+++ b/jbmc/regression/jbmc/destructors/decl.desc
@@ -2,20 +2,20 @@ CORE
 DestructorStackTests
 --show-goto-functions --function DestructorStackTests.mainTest --unwind 10
 activate-multi-line-match
-IF !\(\(int\)unknown == 0\) THEN GOTO [0-9]+[\s]*(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 24 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 50)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+[\s]*\/\/ [0-9]+ no location[\s]*[0-9]+: dead new_tmp[0-9]+;[\s]*
+IF ¬\(.*unknown.* = 0\) THEN GOTO [0-9]+[\s]*(?P<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 24 function java::DestructorStackTests\.mainTest:\(Z\)V bytecode-index 50)[\s]*DEAD .*::new_tmp[0-9]+[\s]*(?P>comment_block)[\s]*GOTO [0-9]+[\s]*\/\/ [0-9]+ no location[\s]*[0-9]+: DEAD .*::new_tmp[0-9]+[\s]*
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
-        IF !((int)unknown == 0) THEN GOTO 1
+        IF ¬(cast(java::DestructorStackTests.mainTest:(Z)V::unknown, signedbv[32]) = 0) THEN GOTO 1
         // 44 file DestructorStackTests.java line 24 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 50
-        dead new_tmp0;
+        DEAD java::DestructorStackTests.mainTest:(Z)V::new_tmp0
         // 45 file DestructorStackTests.java line 24 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 50
         GOTO 2
         // 46 no location
-     1: dead new_tmp0;
+     1: DEAD java::DestructorStackTests.mainTest:(Z)V::new_tmp0
 
 Tests to make sure a declaration kills its temp variable before continuing.
 Numbers vary between symex load / normal load.
diff --git a/jbmc/regression/jbmc/destructors/return.desc b/jbmc/regression/jbmc/destructors/return.desc
index d4bbef0abc3..2ba66288ab3 100644
--- a/jbmc/regression/jbmc/destructors/return.desc
+++ b/jbmc/regression/jbmc/destructors/return.desc
@@ -2,7 +2,7 @@ CORE
 DestructorStackTests
 --show-goto-functions --function DestructorStackTests.mainTest --unwind 10
 activate-multi-line-match
-(?<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 18 function java::DestructorStackTests.mainTest:\(Z\)V bytecode-index 40)[\s]*dead minor[0-9]+;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead anonlocal::[0-9a-zA-Z]+;[\s]*(?P>comment_block)[\s]*dead new_tmp[0-9]+;[\s]*(?P>comment_block)[\s]*dead ex;[\s]*(?P>comment_block)[\s]*dead minor2;[\s]*(?P>comment_block)[\s]*dead minor1;[\s]*(?P>comment_block)[\s]*dead anonlocal::[0-9a-zA-Z]+;[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
+(?<comment_block>\/\/ [0-9]+ file DestructorStackTests\.java line 18 function java::DestructorStackTests.mainTest:\(Z\)V bytecode-index 40)[\s]*DEAD .*::minor[0-9]+[\s]*(?P>comment_block)[\s]*DEAD .*::new_tmp[0-9]+[\s]*(?P>comment_block)[\s]*DEAD .*anonlocal::[0-9a-zA-Z]+[\s]*(?P>comment_block)[\s]*DEAD .*::new_tmp[0-9]+[\s]*(?P>comment_block)[\s]*DEAD .*::ex[\s]*(?P>comment_block)[\s]*DEAD .*::minor2[\s]*(?P>comment_block)[\s]*DEAD .*::minor1[\s]*(?P>comment_block)[\s]*DEAD .*::anonlocal::[0-9a-zA-Z]+[\s]*(?P>comment_block)[\s]*GOTO [0-9]+
 ^EXIT=0$
 ^SIGNAL=0$
 --
@@ -10,21 +10,21 @@ activate-multi-line-match
 Checks for:
 
         // 98 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead minor5;
+        DEAD minor5
         // 99 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead new_tmp6;
+        DEAD new_tmp6
         // 100 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead anonlocal::6a;
+        DEAD anonlocal::6a
         // 101 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead new_tmp5;
+        DEAD new_tmp5
         // 102 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead ex;
+        DEAD ex
         // 103 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead minor2;
+        DEAD minor2
         // 104 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead minor1;
+        DEAD minor1
         // 105 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
-        dead anonlocal::4a;
+        DEAD anonlocal::4a
         // 106 file DestructorStackTests.java line 18 function java::DestructorStackTests.mainTest:(Z)V bytecode-index 40
         GOTO 13
 
diff --git a/jbmc/regression/jbmc/generic_base_type/check_casts.desc b/jbmc/regression/jbmc/generic_base_type/check_casts.desc
index d9b63d75214..667675d620c 100644
--- a/jbmc/regression/jbmc/generic_base_type/check_casts.desc
+++ b/jbmc/regression/jbmc/generic_base_type/check_casts.desc
@@ -3,8 +3,8 @@ Test
 --function Test.main --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-this \. Test\.callee:\(LBase;\)V\(\(struct Base \*\)&return_tmp0->@Base\);
-this \. Test\.callee2:\(LBase;\)V\(&return_tmp1->@Base\);
+CALL java::Test\.callee:\(LBase;\)V\(.*::this, cast\(address_of\(\*java::Test\.main:\(Z\)V::return_tmp0\.@Base\), struct java::Base\*\)\)
+CALL java::Test\.callee2:\(LBase;\)V\(.*::this, address_of\(\*java::Test\.main:\(Z\)V::return_tmp1\.@Base\)\)
 --
 callee has a qualified Base type, and so requires a cast.
 callee2 has the unqualified type that Test<T> naturally inherits, so no cast is required.
diff --git a/jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc b/jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc
index 6c609c1aa92..5247a3e9a50 100644
--- a/jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc
+++ b/jbmc/regression/jbmc/generic_function_parameter/callee2_with_cast.desc
@@ -3,7 +3,7 @@ Test
 --function Test.main2 --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-this \. Test.callee2:\(LTest;\)V\(\(struct Test \*\)param\);
+java::Test.callee2:\(LTest;\)V\(.*::this, cast\(java::Test\.main2:\(LTest;\)V::param, struct java::Test\*\)\)
 --
 --
 Test and callee2 have differing parameter types, so there should be a cast at the callsite.
diff --git a/jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc b/jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc
index 949a81314d2..037e1d38637 100644
--- a/jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc
+++ b/jbmc/regression/jbmc/generic_function_parameter/callee_without_cast.desc
@@ -3,7 +3,7 @@ Test
 --function Test.main --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-this \. Test.callee:\(LTest;\)V\(param\);
+Test.callee:\(LTest;\)V\(.*::this, .*::param\)
 --
 --
 Test and callee have matching parameter types, so there should be no cast at the callsite.
diff --git a/jbmc/regression/jbmc/generic_static_field/test.desc b/jbmc/regression/jbmc/generic_static_field/test.desc
index 6b360e47b60..613b5072557 100644
--- a/jbmc/regression/jbmc/generic_static_field/test.desc
+++ b/jbmc/regression/jbmc/generic_static_field/test.desc
@@ -3,7 +3,7 @@ Test
 --function Test.test --validate-goto-model --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-Test\.test:\(\)LTest;#return_value = static_field;
+ASSIGN java::Test\.test:\(\)LTest;#return_value := java::Test\.static_field$
 --
 ^warning: ignoring
 --
diff --git a/jbmc/regression/jbmc/generic_virtual_function/check_casts.desc b/jbmc/regression/jbmc/generic_virtual_function/check_casts.desc
index 0a0a0902e16..c384eeeca75 100644
--- a/jbmc/regression/jbmc/generic_virtual_function/check_casts.desc
+++ b/jbmc/regression/jbmc/generic_virtual_function/check_casts.desc
@@ -3,10 +3,10 @@ Base
 --function Base.main --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-\(struct Impl1 \*\)b \. Impl1\.f:\(Ljava/lang/Object;\)V\(\(struct java\.lang\.Object \*\)this->genericData\);
-\(struct Impl2 \*\)b \. Impl2\.f:\(Ljava/lang/Object;\)V\(\(struct java\.lang\.Object \*\)this->genericData\);
-\(struct Impl2 \*\)b \. Impl2\.g:\(Ljava/lang/String;\)V\(this->nonGenericData\);
-\(struct Impl1 \*\)b \. Impl1\.g:\(Ljava/lang/String;\)V\(this->nonGenericData\);
+CALL java::Impl1\.f:\(Ljava/lang/Object;\)V\(cast\(.*::b, struct java::Impl1\*\), cast\(\*.*\.genericData, struct java::java\.lang\.Object\*\)\)
+CALL java::Impl2\.f:\(Ljava/lang/Object;\)V\(cast\(.*::b, struct java::Impl2\*\), cast\(\*.*\.genericData, struct java::java\.lang\.Object\*\)\)
+CALL java::Impl2\.g:\(Ljava/lang/String;\)V\(cast\(.*::b, struct java::Impl2\*\), \*.*\.nonGenericData\)
+CALL java::Impl1\.g:\(Ljava/lang/String;\)V\(cast\(.*::b, struct java::Impl1\*\), \*.*\.nonGenericData\)
 --
 --
 Both the implementation classes use a different generic token (Impl1::T and Impl2::T) to refer
diff --git a/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc b/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc
index 190e7a7eac7..20591ac6f00 100644
--- a/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc
+++ b/jbmc/regression/jbmc/lazyloading_no_candidates/test.desc
@@ -4,7 +4,7 @@ Test
 ^EXIT=0$
 ^SIGNAL=0$
 ^CI lazy methods: elaborate java::Test\$intf\.f:\(\)V$
-Test\$intf\.f:\(\)V\(\);$
+Test\$intf\.f:\(\)V\(.*\)$
 --
 --
 This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/reachability-slice/test.desc b/jbmc/regression/jbmc/reachability-slice/test.desc
index 077aa8cd564..c4a9e13e408 100644
--- a/jbmc/regression/jbmc/reachability-slice/test.desc
+++ b/jbmc/regression/jbmc/reachability-slice/test.desc
@@ -3,11 +3,11 @@ A
 --reachability-slice --function A.foo --show-goto-functions --property 'java::A.foo:(I)V.assertion.1'
 ^EXIT=0$
 ^SIGNAL=0$
-= \(int\)\(short\)1001
-= \(int\)\(short\)1002
-= \(int\)\(short\)1003
+:= .*1001
+:= .*1002
+:= .*1003
 --
-= \(int\)\(short\)1004
-= \(int\)\(short\)1005
+:= .*1004
+:= .*1005
 --
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/jbmc/regression/jbmc/reachability-slice/test2.desc b/jbmc/regression/jbmc/reachability-slice/test2.desc
index 083e83fb1ad..f9fffea8fd2 100644
--- a/jbmc/regression/jbmc/reachability-slice/test2.desc
+++ b/jbmc/regression/jbmc/reachability-slice/test2.desc
@@ -3,11 +3,11 @@ A
 --reachability-slice --function A.foo --show-goto-functions --property 'java::A.foo:(I)V.assertion.2'
 ^EXIT=0$
 ^SIGNAL=0$
-= \(int\)\(short\)1001
-= \(int\)\(short\)1004
+:= .*1001
+:= .*1004
 --
-= \(int\)\(short\)1002
-= \(int\)\(short\)1003
-= \(int\)\(short\)1005
+:= .*1002
+:= .*1003
+:= .*1005
 --
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/jbmc/regression/jbmc/reachability-slice/test3.desc b/jbmc/regression/jbmc/reachability-slice/test3.desc
index 62f38772408..e87f7f452da 100644
--- a/jbmc/regression/jbmc/reachability-slice/test3.desc
+++ b/jbmc/regression/jbmc/reachability-slice/test3.desc
@@ -3,11 +3,11 @@ A
 --reachability-slice --function A.foo --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-= \(int\)\(short\)1001
-= \(int\)\(short\)1002
-= \(int\)\(short\)1003
-= \(int\)\(short\)1004
-= \(int\)\(short\)1005
+:= .*1001
+:= .*1002
+:= .*1003
+:= .*1004
+:= .*1005
 --
 --
 Doesn't work with symex-driven lazy loading because the reachability slicer is a whole-program pass.
diff --git a/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc b/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc
index 3396c94d2d5..0c84906c421 100644
--- a/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc
+++ b/jbmc/regression/jbmc/remove_virtual_function_typecast/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 VirtualFunctions
 --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function VirtualFunctions.check --show-goto-functions
- \(struct VirtualFunctions\$B \*\)a \. VirtualFunctions\$B\.f:\(\)V\(\);$
- a \. VirtualFunctions\$A\.f:\(\)V\(\);$
- b \. VirtualFunctions\$B\.f:\(\)V\(\);$
- \(struct VirtualFunctions\$B \*\)c \. VirtualFunctions\$B\.f:\(\)V\(\);$
+CALL java::VirtualFunctions\$B\.f:\(\)V\(cast\(.*::a, struct java::VirtualFunctions\$B\*\)\)$
+CALL java::VirtualFunctions\$A\.f:\(\)V\(.*::a\)$
+CALL java::VirtualFunctions\$B\.f:\(\)V\(.*::b\)$
+CALL java::VirtualFunctions\$B\.f:\(\)V\(cast\(.*::c, struct java::VirtualFunctions\$B\*\)\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/removed_virtual_functions/test.desc b/jbmc/regression/jbmc/removed_virtual_functions/test.desc
index 8207191b63f..a08fc572eb5 100644
--- a/jbmc/regression/jbmc/removed_virtual_functions/test.desc
+++ b/jbmc/regression/jbmc/removed_virtual_functions/test.desc
@@ -1,10 +1,10 @@
 CORE symex-driven-lazy-loading-expected-failure
 ArrayListEquals
 --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --function ArrayListEquals.check2 --show-goto-functions
-e2 . ArrayList\$Itr.hasNext:\(\)Z\(\);
+java::ArrayList\$Itr.hasNext:\(\)Z\(.*\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
-e2 . ListIterator.hasNext:\(\)Z\(\);
+java::ListIterator.hasNext:\(\)Z\(.*\)
 --
 This doesn't work under symex-driven lazy loading because it is incompatible with lazy-methods (default)
diff --git a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_one_candidate.desc b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_one_candidate.desc
index b9e6cf0c0a2..f68db9b732a 100644
--- a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_one_candidate.desc
+++ b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_one_candidate.desc
@@ -3,7 +3,7 @@ Main
 --show-goto-functions --function Main.oneCandidate
 ^EXIT=0$
 ^SIGNAL=0$
-B\.f:\(\)V\(\);$
+B\.f:\(\)V\(.*::b\)$
 --
 this_argument
 --
diff --git a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_no_derefs.desc b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_no_derefs.desc
index aa1943198ef..6a590e44111 100644
--- a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_no_derefs.desc
+++ b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_no_derefs.desc
@@ -3,8 +3,8 @@ Main
 --show-goto-functions --function Main.twoCandidatesNoDerefs
 ^EXIT=0$
 ^SIGNAL=0$
-a \. A\.f:\(\)V\(\);$
-a \. B\.f:\(\)V\(\);$
+CALL java::A\.f:\(\)V\(.*::a\)$
+CALL java::B\.f:\(\)V\(.*::a.*\)$
 --
 this_argument
 --
diff --git a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_with_derefs.desc b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_with_derefs.desc
index d0257dfcde6..a353ec862e8 100644
--- a/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_with_derefs.desc
+++ b/jbmc/regression/jbmc/virtual_temp_var_for_this_argument/test_two_candidates_with_derefs.desc
@@ -3,10 +3,10 @@ Main
 --show-goto-functions --function Main.twoCandidatesWithDerefs
 ^EXIT=0$
 ^SIGNAL=0$
-struct A \*this_argument;$
-this_argument = aContainer->a_field;$
-this_argument \. A\.f:\(\)V\(\);$
-this_argument \. B\.f:\(\)V\(\);$
+DECL .*::this_argument : struct java::A\*$
+ASSIGN .*::this_argument := \*.*::aContainer\.a_field$
+CALL java::A\.f:\(\)V\(.*this_argument.*\)$
+CALL java::B\.f:\(\)V\(.*this_argument.*\)$
 --
 --
 The temporary variable `this_argument` should be created, because it
diff --git a/regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc b/regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc
index 73e2f0b2ffc..a9c36d41d2c 100644
--- a/regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc
+++ b/regression/cbmc-library/string-abstraction/test-c-with-string-abstraction.desc
@@ -1,7 +1,7 @@
 CORE
 test.c
 --string-abstraction --show-goto-functions
-strlen#return_value = \(.*\)s#str->length - POINTER_OFFSET\(s\)\)*;
+ASSIGN strlen#return_value := cast\(cast\(\*strlen::s::s#str\.length, signedbv\[.*\]\) - pointer_offset\(strlen::s\), unsignedbv\[.*\]\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc b/regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc
index 28c456a4bf7..d2b76c017fd 100644
--- a/regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc
+++ b/regression/cbmc-library/string-abstraction/test-c-without-string-abstraction.desc
@@ -1,7 +1,7 @@
 CORE
 test.c
 --show-goto-functions
-IF !\(\(signed int\)s\[\(.*\)len\] != 0\) THEN GOTO 2
+IF ¬\(cast\(\*\(strlen::s \+ cast\(strlen::1::len, signedbv\[.*\]\)\), signedbv\[32\]\) ≠ 0\) THEN GOTO 2
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc/destructors/compound_literal.desc b/regression/cbmc/destructors/compound_literal.desc
index 46640b2c02c..47c217fed18 100644
--- a/regression/cbmc/destructors/compound_literal.desc
+++ b/regression/cbmc/destructors/compound_literal.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*dead newAlloc0;[\s]*(?P>comment_block)[\s]*dead pc;[\s]*(?P>comment_block)[\s]*dead literal;[\s]*(?P>comment_block)[\s]*9: END_FUNCTION
+(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*9: END_FUNCTION
 ^EXIT=0$
 ^SIGNAL=0$
 --
@@ -10,11 +10,11 @@ activate-multi-line-match
 Checks for:
 
        // 49 file main.c line 44 function main
-       dead newAlloc0;
+       DEAD main::1::newAlloc0
        // 50 file main.c line 44 function main
-       dead pc;
+       DEAD main::1::pc
        // 51 file main.c line 44 function main
-       dead literal;
+       DEAD main::$tmp::literal
        // 52 file main.c line 45 function main
     9: END_FUNCTION
 
diff --git a/regression/cbmc/destructors/enter_lexical_block.desc b/regression/cbmc/destructors/enter_lexical_block.desc
index 3f02325816d..751e929d85d 100644
--- a/regression/cbmc/destructors/enter_lexical_block.desc
+++ b/regression/cbmc/destructors/enter_lexical_block.desc
@@ -2,26 +2,26 @@ CORE
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: test newAlloc4;[\s]*(?P>comment_block)[\s]*newAlloc4 = \{ \.id=4 \};[\s]*(?P>comment_block)[\s]*test newAlloc6;[\s]*(?P>comment_block)[\s]*newAlloc6 = \{ \.id=6 \};[\s]*(?P>comment_block)[\s]*test newAlloc7;[\s]*(?P>comment_block)[\s]*newAlloc7 = \{ \.id=7 \};[\s]*(?P>comment_block)[\s]*GOTO 3
+(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*GOTO 3
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
-       // 31 file main.c line 34 function main
-    6: test newAlloc4;
-       // 32 file main.c line 34 function main
-       newAlloc4 = { .id=4 };
-       // 33 file main.c line 35 function main
-       test newAlloc6;
-       // 34 file main.c line 35 function main
-       newAlloc6 = { .id=6 };
-       // 35 file main.c line 36 function main
-       test newAlloc7;
-       // 36 file main.c line 36 function main
-       newAlloc7 = { .id=7 };
-       // 37 file main.c line 37 function main
+       // 37 file main.c line 36 function main
+    6: DECL main::1::2::2::newAlloc4 : struct tag-test
+       // 38 file main.c line 36 function main
+       ASSIGN main::1::2::2::newAlloc4 := { 4 }
+       // 39 file main.c line 37 function main
+       DECL main::1::2::2::newAlloc6 : struct tag-test
+       // 40 file main.c line 37 function main
+       ASSIGN main::1::2::2::newAlloc6 := { 6 }
+       // 41 file main.c line 38 function main
+       DECL main::1::2::2::newAlloc7 : struct tag-test
+       // 42 file main.c line 38 function main
+       ASSIGN main::1::2::2::newAlloc7 := { 7 }
+       // 43 file main.c line 39 function main
        GOTO 3
 
 This asserts that when the GOTO is going into a lexical block that destructors
diff --git a/regression/cbmc/reachability-slice-interproc3/test.desc b/regression/cbmc/reachability-slice-interproc3/test.desc
index f2af4dc0176..66f6ca60700 100644
--- a/regression/cbmc/reachability-slice-interproc3/test.desc
+++ b/regression/cbmc/reachability-slice-interproc3/test.desc
@@ -3,6 +3,6 @@ main.c
 --reachability-slice-fb --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
-main#return_value = 1;
+ASSIGN main#return_value := 1
 --
 ^warning: ignoring
diff --git a/regression/contracts/assigns_validity_pointer_01/test.desc b/regression/contracts/assigns_validity_pointer_01/test.desc
index 345bde8483c..9ef4d9894d7 100644
--- a/regression/contracts/assigns_validity_pointer_01/test.desc
+++ b/regression/contracts/assigns_validity_pointer_01/test.desc
@@ -6,19 +6,19 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 SUCCESS
 // bar
-ASSERT \*x > 0
-IF !\(\*x == 3\) THEN GOTO \d
-IF !\(\(signed int \*\)\(void \*\)0 == \(\(signed int \*\)NULL\)\) THEN GOTO \d
-tmp_if_expr = \*\(\(signed int \*\)\(void \*\)0\) == 5 \? TRUE \: FALSE;
-tmp_if_expr\$\d = tmp_if_expr \? TRUE : FALSE;
-ASSUME tmp_if_expr\$\d
+ASSERT \*foo::x > 0
+IF ¬\(\*foo::x = 3\) THEN GOTO \d
+IF ¬\(.*0.* = NULL\) THEN GOTO \d
+ASSIGN .*::tmp_if_expr := \(\*\(.*0.*\) = 5 \? true : false\)
+ASSIGN .*::tmp_if_expr\$\d := .*::tmp_if_expr \? true : false
+ASSUME .*::tmp_if_expr\$\d
 // baz
-IF !\(z == \(\(signed int \*\)NULL\)\) THEN GOTO \d
-tmp_if_expr\$\d = \*z == 7 \? TRUE : FALSE;
-ASSUME tmp_if_expr\$\d
+IF ¬\(z ≠ NULL\) THEN GOTO \d
+ASSIGN .*::tmp_if_expr\$\d := \(\*z = 7 \? true : false\)
+ASSUME .*::tmp_if_expr\$\d
 // foo
-ASSUME \*tmp_cc\$\d > 0
-ASSERT \*tmp_cc\$\d == 3
+ASSUME \*.*::tmp_cc\$\d > 0
+ASSERT \*.*::tmp_cc\$\d = 3
 --
 \[3\] file main\.c line 6 assertion: FAILURE
 --
diff --git a/regression/contracts/assigns_validity_pointer_02/test.desc b/regression/contracts/assigns_validity_pointer_02/test.desc
index 038910fa7bf..ebfee6dc26a 100644
--- a/regression/contracts/assigns_validity_pointer_02/test.desc
+++ b/regression/contracts/assigns_validity_pointer_02/test.desc
@@ -6,8 +6,8 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 //^([foo\.1] line 15 assertion: FAILURE)
 // foo
-ASSUME \*tmp_cc\$\d > 0
-ASSERT \*tmp_cc\$\d == 3
+ASSUME \*.*::tmp_cc\$\d > 0
+ASSERT \*.*::tmp_cc\$\d = 3
 --
 \[foo\.1\] line 24 assertion: FAILURE
 \[foo\.3\] line 27 assertion: FAILURE
diff --git a/regression/contracts/assigns_validity_pointer_03/test.desc b/regression/contracts/assigns_validity_pointer_03/test.desc
index 988ad466d7c..7c04f9cff70 100644
--- a/regression/contracts/assigns_validity_pointer_03/test.desc
+++ b/regression/contracts/assigns_validity_pointer_03/test.desc
@@ -7,7 +7,7 @@ main.c
 // bar
 ASSERT \*x > 0
 IF !\(\*x == 3\) THEN GOTO \d
-tmp_if_expr = \*y == 5 \? TRUE \: FALSE;
+tmp_if_expr = \*y == 5 \? true \: false;
 ASSUME tmp_if_expr
 // baz
 ASSUME \*z == 7
diff --git a/regression/contracts/assigns_validity_pointer_04/test.desc b/regression/contracts/assigns_validity_pointer_04/test.desc
index f6cee72a7b6..11aec0dea4b 100644
--- a/regression/contracts/assigns_validity_pointer_04/test.desc
+++ b/regression/contracts/assigns_validity_pointer_04/test.desc
@@ -5,15 +5,15 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 // bar
-ASSERT \*x > 0
-IF !\(\*x == 3\) THEN GOTO \d
-tmp_if_expr = \*y == 5 \? TRUE \: FALSE;
-ASSUME tmp_if_expr
+ASSERT \*foo::x > 0
+IF ¬\(\*foo::x = 3\) THEN GOTO \d
+ASSIGN goto_convertt::tmp_if_expr := \(\*foo::1::y = 5 \? true : false\)
+ASSUME .*::tmp_if_expr
 // baz
-ASSUME \*z == 7
+ASSUME \*z = 7
 // foo
-ASSUME \*tmp_cc\$\d > 0
-ASSERT \*tmp_cc\$\d == 3
+ASSUME \*.*::tmp_cc\$\d > 0
+ASSERT \*.*::tmp_cc\$\d = 3
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-both-01/test.desc b/regression/contracts/history-pointer-both-01/test.desc
index 76377d45f8a..edc7af0ddcd 100644
--- a/regression/contracts/history-pointer-both-01/test.desc
+++ b/regression/contracts/history-pointer-both-01/test.desc
@@ -4,10 +4,10 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-ASSUME tmp_cc\$\d != \(\(signed int \*\)NULL\)
-ASSERT n != \(\(signed int \*\)NULL\)
-ASSUME tmp_cc == \*n
-ASSERT tmp_cc\$\d == \*tmp_cc\$\d
+ASSUME .*::tmp_cc\$\d ≠ NULL
+ASSERT foo::n ≠ NULL
+ASSUME .*::tmp_cc = \*foo::n
+ASSERT .*::tmp_cc\$\d = \*.*::tmp_cc\$\d
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-enforce-01/test.desc b/regression/contracts/history-pointer-enforce-01/test.desc
index d3300daed5c..594cb8af05d 100644
--- a/regression/contracts/history-pointer-enforce-01/test.desc
+++ b/regression/contracts/history-pointer-enforce-01/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-ASSERT \*tmp_cc\$\d == tmp_cc\$\d \+ 5
+ASSERT \*.*::tmp_cc\$\d = .*::tmp_cc\$\d \+ 5
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-enforce-02/test.desc b/regression/contracts/history-pointer-enforce-02/test.desc
index 960b0eb4aaf..bd08337d8ee 100644
--- a/regression/contracts/history-pointer-enforce-02/test.desc
+++ b/regression/contracts/history-pointer-enforce-02/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-ASSERT \*tmp_cc\$\d < tmp_cc\$\d \+ 5
+ASSERT \*.*::tmp_cc\$\d < .*::tmp_cc\$\d \+ 5
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-enforce-03/test.desc b/regression/contracts/history-pointer-enforce-03/test.desc
index 9938b262b58..dc32ca22c00 100644
--- a/regression/contracts/history-pointer-enforce-03/test.desc
+++ b/regression/contracts/history-pointer-enforce-03/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-ASSERT tmp_if_expr\$\d
+ASSERT .*::tmp_if_expr\$\d
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-enforce-04/test.desc b/regression/contracts/history-pointer-enforce-04/test.desc
index 21bab515511..4ff79ee01ca 100644
--- a/regression/contracts/history-pointer-enforce-04/test.desc
+++ b/regression/contracts/history-pointer-enforce-04/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-ASSERT tmp_if_expr
+ASSERT .*::tmp_if_expr
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-enforce-05/test.desc b/regression/contracts/history-pointer-enforce-05/test.desc
index 493944290e8..5606d2d5856 100644
--- a/regression/contracts/history-pointer-enforce-05/test.desc
+++ b/regression/contracts/history-pointer-enforce-05/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-ASSERT tmp_if_expr
+ASSERT .*::tmp_if_expr
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-enforce-08/test.desc b/regression/contracts/history-pointer-enforce-08/test.desc
index 951fff65c6f..9049c0bc86c 100644
--- a/regression/contracts/history-pointer-enforce-08/test.desc
+++ b/regression/contracts/history-pointer-enforce-08/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-ASSERT \*tmp_cc\$\d\.y == tmp_cc\$\d \+ 5
+ASSERT \*\(.*::tmp_cc\$\d\.y\) = .*::tmp_cc\$\d \+ 5
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-replace-01/test.desc b/regression/contracts/history-pointer-replace-01/test.desc
index 3c047fc5975..611dfd7552a 100644
--- a/regression/contracts/history-pointer-replace-01/test.desc
+++ b/regression/contracts/history-pointer-replace-01/test.desc
@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-ASSERT \*\(&n\) > 0
-ASSUME \*\(&n\) == tmp_cc[\$\d]? \+ 2
+ASSERT \*\(address_of.*n.*\) > 0
+ASSUME \*\(address_of.*n.*\) = .*::tmp_cc[\$\d]? \+ 2
 --
 --
 Verification:
diff --git a/regression/contracts/history-pointer-replace-02/test.desc b/regression/contracts/history-pointer-replace-02/test.desc
index 3903c0aa6ff..68dea109f7f 100644
--- a/regression/contracts/history-pointer-replace-02/test.desc
+++ b/regression/contracts/history-pointer-replace-02/test.desc
@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-ASSERT \*\(&n\) == 0
-ASSUME \*\(&n\) >= tmp_cc[\$\d]? \+ 2
+ASSERT \*\(address_of.*n.*\) = 0
+ASSUME \*\(address_of.*n.*\) ≥ .*::tmp_cc[\$\d]? \+ 2
 --
 --
 Verification:
diff --git a/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc b/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc
index 40eb8d1a1b4..823418a6ed3 100644
--- a/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc
+++ b/regression/goto-analyzer-simplify/simplify-complex-expression/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --vsd
-r == 2
+r = 2
 ^SIGNAL=0$
 ^EXIT=0$
 --
diff --git a/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc
index d1161d20eff..5f1ac78c109 100644
--- a/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc
+++ b/regression/goto-analyzer-simplify/simplify-lhs-array-index/test.desc
@@ -1,9 +1,9 @@
 CORE
 main.c
 --vsd --vsd-arrays every-element
-arr\[0l?l?\] =
-arr\[1l?l?\] =
-arr\[\(signed (long (long )?)?int\)nondet\] =
+arr\[0\] :=
+arr\[1\] :=
+arr\[.*nondet.*\] :=
 ^SIGNAL=0$
 ^EXIT=0$
 --
diff --git a/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc
index 715e8782c58..9e70e14c974 100644
--- a/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc
+++ b/regression/goto-analyzer-simplify/simplify-lhs-array-pointers-index/test.desc
@@ -1,10 +1,10 @@
 CORE
 main.c
 --vsd --vsd-arrays every-element --vsd-pointers value-set
-symbol_a = 1
-symbol_b = 2
-\*arr\[2l?l?\] = 3;
-\*arr\[\(signed (long (long )?)?int\)nondet_index\] = 4;
+symbol_a := 1
+symbol_b := 2
+\*\(.*::arr\[2\]\) := 3
+\*\(.*::arr\[.*nondet_index.*\]\) := 4
 ^SIGNAL=0$
 ^EXIT=0$
 --
diff --git a/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc
index e7dc545e387..bfe42612579 100644
--- a/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc
+++ b/regression/goto-analyzer-simplify/simplify-lhs-dereference/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --vsd --vsd-pointers value-set
-symbol = 5
-\*pointer = 6
+symbol := 5
+\*.*::pointer := 6
 ^SIGNAL=0$
 ^EXIT=0$
 --
diff --git a/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc
index e9181e3e47a..e3b1a22b2da 100644
--- a/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc
+++ b/regression/goto-analyzer-simplify/simplify-lhs-member/test.desc
@@ -1,10 +1,10 @@
 CORE
 main.c
 --vsd --vsd-arrays every-element --vsd-pointers value-set --vsd-structs every-field
-symbol = 5
-\*value\.pointer_component = 6
-value\.array\[1l?l?\] = 2
-value\.array\[\(signed (long (long )?)?int\)nondet\] = 3
+symbol := 5
+\*\(.*::value\.pointer_component\) := 6
+value\.array\[1\] := 2
+value\.array\[.*nondet.*\] := 3
 ^SIGNAL=0$
 ^EXIT=0$
 --
diff --git a/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc b/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc
index f5bb0f7c897..ce92a68e65e 100644
--- a/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc
+++ b/regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/test.desc
@@ -1,9 +1,9 @@
 CORE
 main.c
 --vsd --vsd-arrays every-element --vsd-pointers value-set
-array\[0l?l?\] = 5
-array\[\(signed (long (long )?)?int\)nondet\] = 6
-new_array\[1l?l?\] = 7
+array\[0\] := 5
+array\[.*nondet.*\] := 6
+new_array\[1\] := 7
 ^SIGNAL=0$
 ^EXIT=0$
 --
diff --git a/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc b/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc
index 59ae86c6ccf..2263eb791f3 100644
--- a/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc
+++ b/regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc
@@ -3,7 +3,7 @@ main.c
 --vsd
 ^SIGNAL=0$
 ^EXIT=0$
-main#return_value = 0;
+main#return_value := 0
 --
 --
 Tests that a multiplication
diff --git a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc
index 82860e90e86..ff396910001 100644
--- a/regression/goto-analyzer/approx-array-variable-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-array-variable-const-fp/test.desc
@@ -2,17 +2,17 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp_tbl\[.*i\] == f2 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f3 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f4 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f4\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
-^\s*IF fp_tbl\[.*i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$
 ^warning: ignoring
 function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc
index 5b970303b37..e6adfd16987 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-cast-const-fp/test.desc
@@ -2,17 +2,17 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc
index bd1f5b41a5d..20b56e58877 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp-with-null/test.desc
@@ -2,18 +2,18 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
 replacing function pointer by 3 possible targets
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc
index 5b970303b37..c2e7c0b8632 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-fp/test.desc
@@ -2,17 +2,17 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
index 5b970303b37..c9b7b3375f1 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
@@ -2,17 +2,17 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] == address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] == address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] == address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] == address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] == address_of\(f9\) THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc
index 5b970303b37..c2e7c0b8632 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-const-struct-non-const-fp/test.desc
@@ -2,17 +2,17 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc
index 57386e3d576..8952e72ccd3 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc
@@ -2,17 +2,17 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == \(.*\)f2 THEN GOTO [0-9]$
-^\s*IF fp == \(.*\)f3 THEN GOTO [0-9]$
-^\s*IF fp == \(.*\)f4 THEN GOTO [0-9]$
+^\s*IF .*::fp = .*f2.* THEN GOTO [0-9]$
+^\s*IF .*::fp = .*f3.* THEN GOTO [0-9]$
+^\s*IF .*::fp = .*f4.* THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed( long)? long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] == f9 THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
index b687a13cf86..5d052a3dd17 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
@@ -2,18 +2,18 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*ASSERT FALSE // invalid function pointer$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*ASSERT false // invalid function pointer$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 function \w+: replacing function pointer by 9 possible targets
diff --git a/regression/goto-analyzer/dependence-graph10/test.desc b/regression/goto-analyzer/dependence-graph10/test.desc
index 26943fc2e68..d079970cac5 100644
--- a/regression/goto-analyzer/dependence-graph10/test.desc
+++ b/regression/goto-analyzer/dependence-graph10/test.desc
@@ -5,9 +5,9 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 // First assignment has a control dependency on the if
-\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1
+\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 1
 // Second assignment has a control dependency on the if
-\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2
+\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 2
 --
 ^warning: ignoring
 --
diff --git a/regression/goto-analyzer/dependence-graph11/test.desc b/regression/goto-analyzer/dependence-graph11/test.desc
index 32969498ac0..efb84f1b68b 100644
--- a/regression/goto-analyzer/dependence-graph11/test.desc
+++ b/regression/goto-analyzer/dependence-graph11/test.desc
@@ -5,7 +5,7 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 // Assignment has a control dependency on the if
-\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1
+\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 1
 --
 ^warning: ignoring
 --
diff --git a/regression/goto-analyzer/dependence-graph12/test.desc b/regression/goto-analyzer/dependence-graph12/test.desc
index 419f4efc4e1..886247aa9c6 100644
--- a/regression/goto-analyzer/dependence-graph12/test.desc
+++ b/regression/goto-analyzer/dependence-graph12/test.desc
@@ -5,9 +5,9 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 // Assignment has a control dependency on the first if
-\/\/ ([0-9]+).*\n.*IF.*a < 7.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2
+\/\/ ([0-9]+).*\n.*IF.*a < 7.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a := 2
 // Assignment has a control dependency on the second if
-\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2
+\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a := 2
 --
 ^warning: ignoring
 --
diff --git a/regression/goto-analyzer/dependence-graph14/test.desc b/regression/goto-analyzer/dependence-graph14/test.desc
index c00f0acd68a..e2d43d71192 100644
--- a/regression/goto-analyzer/dependence-graph14/test.desc
+++ b/regression/goto-analyzer/dependence-graph14/test.desc
@@ -4,9 +4,9 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\/\/ ([0-9]+).*\n.*a\[(\(signed long( long)? int\))?2\] = 2;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = *
+\/\/ ([0-9]+).*\n.*::a\[.*2.*\] := 2(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out := .*
 --
-\/\/ ([0-9]+).*\n.*a\[(\(signed long( long)? int\))?1\] = 1;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = *
+\/\/ ([0-9]+).*\n.*::a\[.*1.*\] := 1(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out := .*
 ^warning: ignoring
 --
 
diff --git a/regression/goto-analyzer/dependence-graph4/test.desc b/regression/goto-analyzer/dependence-graph4/test.desc
index 670220ddf98..37849b77ce7 100644
--- a/regression/goto-analyzer/dependence-graph4/test.desc
+++ b/regression/goto-analyzer/dependence-graph4/test.desc
@@ -4,7 +4,7 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\/\/ ([0-9]+) file.*\n.*IF.*g_in1.*THEN GOTO(.*\n)*Control dependencies: \1\n\n.*\n.*g_out = 1
+\/\/ ([0-9]+) file.*\n.*IF.*g_in1.*THEN GOTO(.*\n)*Control dependencies: \1\n\n.*\n.*g_out := 1
 --
 ^warning: ignoring
 --
diff --git a/regression/goto-analyzer/dependence-graph7/test.desc b/regression/goto-analyzer/dependence-graph7/test.desc
index 80a11db5a17..fbc0a0b72c4 100644
--- a/regression/goto-analyzer/dependence-graph7/test.desc
+++ b/regression/goto-analyzer/dependence-graph7/test.desc
@@ -5,7 +5,7 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 // Assignment has a control dependency on the loop head
-\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1
+\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 1
 // Backedge has a control dependency on the loop head
 \/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}\s*GOTO [0-9]+
 // Loop head has a control dependency on itself
diff --git a/regression/goto-analyzer/dependence-graph8/test.desc b/regression/goto-analyzer/dependence-graph8/test.desc
index 50a092d6d9e..c6536ffd3ac 100644
--- a/regression/goto-analyzer/dependence-graph8/test.desc
+++ b/regression/goto-analyzer/dependence-graph8/test.desc
@@ -5,7 +5,7 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 // Assignment has a control dependency on the if
-\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1
+\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 1
 // If has a control dependency on the loop head
 \/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*i < 7
 --
diff --git a/regression/goto-analyzer/dependence-graph9/test.desc b/regression/goto-analyzer/dependence-graph9/test.desc
index c6dd50d71cb..cc445547750 100644
--- a/regression/goto-analyzer/dependence-graph9/test.desc
+++ b/regression/goto-analyzer/dependence-graph9/test.desc
@@ -5,11 +5,11 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 // Second assignment has a control dependency on the outer if
-\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2
+\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 2
 --
 ^warning: ignoring
 // Second assignment does not have a control dependency on the inner if
-\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2
+\/\/ ([0-9]+).*\n.*IF.*i < 7.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a := 2
 --
 The first regex above matches output portions like shown below (with <N> being a
 location number). The intention is to check whether the assignment has a control
diff --git a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc
index 25c0e72dadf..d42046c6e62 100644
--- a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc
+++ b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT FALSE // invalid function pointer$
+^\s*ASSERT false // invalid function pointer$
 ^EXIT=0$
 ^SIGNAL=0$
 function func: replacing function pointer by 0 possible targets
diff --git a/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc b/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc
index a439885fc9c..249a6403ecd 100644
--- a/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc
+++ b/regression/goto-analyzer/no-match-const-array-const-pointer-const-fp-const-lost/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF \*fp == f1 THEN GOTO [0-9]$
-^\s*IF \*fp == f2 THEN GOTO [0-9]$
-^\s*IF \*fp == f3 THEN GOTO [0-9]$
-^\s*IF \*fp == f4 THEN GOTO [0-9]$
-^\s*IF \*fp == f5 THEN GOTO [0-9]$
-^\s*IF \*fp == f6 THEN GOTO [0-9]$
-^\s*IF \*fp == f7 THEN GOTO [0-9]$
-^\s*IF \*fp == f8 THEN GOTO [0-9]$
-^\s*IF \*fp == f9 THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-array-literal-const-fp-run-time/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp-run-time/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc
index 1fb62392ced..3a415cc88c6 100644
--- a/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-array-literal-non-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp2 == f1 THEN GOTO [0-9]$
-^\s*IF fp2 == f2 THEN GOTO [0-9]$
-^\s*IF fp2 == f3 THEN GOTO [0-9]$
-^\s*IF fp2 == f4 THEN GOTO [0-9]$
-^\s*IF fp2 == f5 THEN GOTO [0-9]$
-^\s*IF fp2 == f6 THEN GOTO [0-9]$
-^\s*IF fp2 == f7 THEN GOTO [0-9]$
-^\s*IF fp2 == f8 THEN GOTO [0-9]$
-^\s*IF fp2 == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc
index 1fb62392ced..3a415cc88c6 100644
--- a/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-array-non-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp2 == f1 THEN GOTO [0-9]$
-^\s*IF fp2 == f2 THEN GOTO [0-9]$
-^\s*IF fp2 == f3 THEN GOTO [0-9]$
-^\s*IF fp2 == f4 THEN GOTO [0-9]$
-^\s*IF fp2 == f5 THEN GOTO [0-9]$
-^\s*IF fp2 == f6 THEN GOTO [0-9]$
-^\s*IF fp2 == f7 THEN GOTO [0-9]$
-^\s*IF fp2 == f8 THEN GOTO [0-9]$
-^\s*IF fp2 == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-binary-op-const-lost/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc
index a439885fc9c..249a6403ecd 100644
--- a/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-const-array-index-lost/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF \*fp == f1 THEN GOTO [0-9]$
-^\s*IF \*fp == f2 THEN GOTO [0-9]$
-^\s*IF \*fp == f3 THEN GOTO [0-9]$
-^\s*IF \*fp == f4 THEN GOTO [0-9]$
-^\s*IF \*fp == f5 THEN GOTO [0-9]$
-^\s*IF \*fp == f6 THEN GOTO [0-9]$
-^\s*IF \*fp == f7 THEN GOTO [0-9]$
-^\s*IF \*fp == f8 THEN GOTO [0-9]$
-^\s*IF \*fp == f9 THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc
index a439885fc9c..249a6403ecd 100644
--- a/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-const-array-lost/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF \*fp == f1 THEN GOTO [0-9]$
-^\s*IF \*fp == f2 THEN GOTO [0-9]$
-^\s*IF \*fp == f3 THEN GOTO [0-9]$
-^\s*IF \*fp == f4 THEN GOTO [0-9]$
-^\s*IF \*fp == f5 THEN GOTO [0-9]$
-^\s*IF \*fp == f6 THEN GOTO [0-9]$
-^\s*IF \*fp == f7 THEN GOTO [0-9]$
-^\s*IF \*fp == f8 THEN GOTO [0-9]$
-^\s*IF \*fp == f9 THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF \*.*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc b/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-const-cast/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc
index da6211eba82..6072f5b10f4 100644
--- a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT FALSE // invalid function pointer$
+^\s*ASSERT false // invalid function pointer$
 ^EXIT=0$
 ^SIGNAL=0$
 replacing function pointer by 0 possible targets
diff --git a/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-const-lost/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc
index 24ca16f13c1..35d7e0bfdc0 100644
--- a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT FALSE // invalid function pointer$
+^\s*ASSERT false // invalid function pointer$
 replacing function pointer by 9 possible targets
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-non-const-struct-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc
index 24ca16f13c1..35d7e0bfdc0 100644
--- a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT FALSE // invalid function pointer$
+^\s*ASSERT false // invalid function pointer$
 replacing function pointer by 9 possible targets
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc
index 4b204902e0b..30fd992061e 100644
--- a/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-dereference-non-const-pointer-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF final_fp == f1 THEN GOTO [0-9]$
-^\s*IF final_fp == f2 THEN GOTO [0-9]$
-^\s*IF final_fp == f3 THEN GOTO [0-9]$
-^\s*IF final_fp == f4 THEN GOTO [0-9]$
-^\s*IF final_fp == f5 THEN GOTO [0-9]$
-^\s*IF final_fp == f6 THEN GOTO [0-9]$
-^\s*IF final_fp == f7 THEN GOTO [0-9]$
-^\s*IF final_fp == f8 THEN GOTO [0-9]$
-^\s*IF final_fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::final_fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::final_fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::final_fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::final_fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::final_fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::final_fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::final_fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::final_fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::final_fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc
index c1c2246e027..4548ea5c4c8 100644
--- a/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-dynamic-array-non-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]+$
-^\s*IF fp == f2 THEN GOTO [0-9]+$
-^\s*IF fp == f3 THEN GOTO [0-9]+$
-^\s*IF fp == f4 THEN GOTO [0-9]+$
-^\s*IF fp == f5 THEN GOTO [0-9]+$
-^\s*IF fp == f6 THEN GOTO [0-9]+$
-^\s*IF fp == f7 THEN GOTO [0-9]+$
-^\s*IF fp == f8 THEN GOTO [0-9]+$
-^\s*IF fp == f9 THEN GOTO [0-9]+$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]+$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]+$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]+$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]+$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]+$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]+$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]+$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]+$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]+$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc
index 1fb62392ced..3a415cc88c6 100644
--- a/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-non-const-fp-direct-assignment/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp2 == f1 THEN GOTO [0-9]$
-^\s*IF fp2 == f2 THEN GOTO [0-9]$
-^\s*IF fp2 == f3 THEN GOTO [0-9]$
-^\s*IF fp2 == f4 THEN GOTO [0-9]$
-^\s*IF fp2 == f5 THEN GOTO [0-9]$
-^\s*IF fp2 == f6 THEN GOTO [0-9]$
-^\s*IF fp2 == f7 THEN GOTO [0-9]$
-^\s*IF fp2 == f8 THEN GOTO [0-9]$
-^\s*IF fp2 == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-non-const-pointer-non-const-struct-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-non-const-struct-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-non-const-struct-non-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-null/test.desc
index 0abb9994d73..9fdf5e55158 100644
--- a/regression/goto-analyzer/no-match-const-fp-null/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT FALSE // invalid function pointer$
+^\s*ASSERT false // invalid function pointer$
 function func: replacing function pointer by 0 possible targets
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc b/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc
+++ b/regression/goto-analyzer/no-match-const-fp-ternerary-op-const-lost/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc b/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc
index 39b4bf06fa6..83bb08b57d9 100644
--- a/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc
+++ b/regression/goto-analyzer/no-match-const-pointer-const-struct-const-fp-const-cast/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF container_pointer->fp == f1 THEN GOTO [0-9]$
-^\s*IF container_pointer->fp == f2 THEN GOTO [0-9]$
-^\s*IF container_pointer->fp == f3 THEN GOTO [0-9]$
-^\s*IF container_pointer->fp == f4 THEN GOTO [0-9]$
-^\s*IF container_pointer->fp == f5 THEN GOTO [0-9]$
-^\s*IF container_pointer->fp == f6 THEN GOTO [0-9]$
-^\s*IF container_pointer->fp == f7 THEN GOTO [0-9]$
-^\s*IF container_pointer->fp == f8 THEN GOTO [0-9]$
-^\s*IF container_pointer->fp == f9 THEN GOTO [0-9]$
+^\s*IF .*container_pointer\.fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*container_pointer\.fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*container_pointer\.fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*container_pointer\.fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*container_pointer\.fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*container_pointer\.fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*container_pointer\.fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*container_pointer\.fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*container_pointer\.fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc b/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc
index c2854d7bb90..32128bfe112 100644
--- a/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-const-pointer-non-const-struct-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF pts->go == f1 THEN GOTO [0-9]$
-^\s*IF pts->go == f2 THEN GOTO [0-9]$
-^\s*IF pts->go == f3 THEN GOTO [0-9]$
-^\s*IF pts->go == f4 THEN GOTO [0-9]$
-^\s*IF pts->go == f5 THEN GOTO [0-9]$
-^\s*IF pts->go == f6 THEN GOTO [0-9]$
-^\s*IF pts->go == f7 THEN GOTO [0-9]$
-^\s*IF pts->go == f8 THEN GOTO [0-9]$
-^\s*IF pts->go == f9 THEN GOTO [0-9]$
+^\s*IF .*pts\.go = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*pts\.go = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*pts\.go = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*pts\.go = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*pts\.go = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*pts\.go = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*pts\.go = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*pts\.go = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*pts\.go = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc
index da6211eba82..6072f5b10f4 100644
--- a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc
+++ b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT FALSE // invalid function pointer$
+^\s*ASSERT false // invalid function pointer$
 ^EXIT=0$
 ^SIGNAL=0$
 replacing function pointer by 0 possible targets
diff --git a/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc
index 63c375d058a..90e20e43fc4 100644
--- a/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF \*container_ptr->fp_tbl\[.*1\] == f1 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[.*1\] == f2 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[.*1\] == f3 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[.*1\] == f4 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[.*1\] == f5 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[.*1\] == f6 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[.*1\] == f7 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[.*1\] == f8 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[.*1\] == f9 THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_ptr.fp_tbl\[.*1.*\]\) = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc
index 7c7f7c5d265..7bb43ba7876 100644
--- a/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-dereference-non-const-struct-const-pointer-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF \*container_container\.container == f1 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f2 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f3 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f4 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f5 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f6 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f7 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f8 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f9 THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc b/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc
index 7c7f7c5d265..7bb43ba7876 100644
--- a/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-dereference-non-const-struct-non-const-pointer-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF \*container_container\.container == f1 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f2 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f3 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f4 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f5 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f6 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f7 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f8 THEN GOTO [0-9]$
-^\s*IF \*container_container\.container == f9 THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF \*\(.*::container_container\.container\) = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc b/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc
index 1fb62392ced..3a415cc88c6 100644
--- a/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc
+++ b/regression/goto-analyzer/no-match-non-const-fp-const-fp-direct-assignment/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp2 == f1 THEN GOTO [0-9]$
-^\s*IF fp2 == f2 THEN GOTO [0-9]$
-^\s*IF fp2 == f3 THEN GOTO [0-9]$
-^\s*IF fp2 == f4 THEN GOTO [0-9]$
-^\s*IF fp2 == f5 THEN GOTO [0-9]$
-^\s*IF fp2 == f6 THEN GOTO [0-9]$
-^\s*IF fp2 == f7 THEN GOTO [0-9]$
-^\s*IF fp2 == f8 THEN GOTO [0-9]$
-^\s*IF fp2 == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp2 = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-non-const-fp/test.desc b/regression/goto-analyzer/no-match-non-const-fp/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-non-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-non-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-parameter-const-fp/test.desc b/regression/goto-analyzer/no-match-parameter-const-fp/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-parameter-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-parameter-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-parameter-fp/test.desc b/regression/goto-analyzer/no-match-parameter-fp/test.desc
index 9fc199c2365..2335ab71d77 100644
--- a/regression/goto-analyzer/no-match-parameter-fp/test.desc
+++ b/regression/goto-analyzer/no-match-parameter-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc b/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc
index ca24699d5a0..5dd35ba8d55 100644
--- a/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc
+++ b/regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc
@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*IF container_ptr->fp_tbl\[.*1\] == f1 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[.*1\] == f2 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[.*1\] == f3 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[.*1\] == f4 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[.*1\] == f5 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[.*1\] == f6 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[.*1\] == f7 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[.*1\] == f8 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[.*1\] == f9 THEN GOTO [0-9]$
+^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*container_ptr\.fp_tbl\[.*1.*\] = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-array-calculation-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-array-literal-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-array-literal-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-array-const-variable-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp-run-time/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-array-literal-const-struct-non-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
index 791dbe0703c..f6359140fef 100644
--- a/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-array-variable-const-pointer-const-struct-non-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f2\(\);
+^\s*CALL f2\(\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc
index 479c26e4afe..a5e81889688 100644
--- a/regression/goto-analyzer/precise-const-fp-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f2\(\);$
+^\s*CALL f2\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-const-struct-const-array-literal-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-array-literal-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc
index 791dbe0703c..f6359140fef 100644
--- a/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-const-struct-non-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f2\(\);
+^\s*CALL f2\(\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-dereference-const-pointer-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc b/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc
index 15fc1e17ef7..a36c3f3a4fc 100644
--- a/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc
+++ b/regression/goto-analyzer/precise-const-fp-supurious-const-loss/test.desc
@@ -2,19 +2,19 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f2\(\);
+^\s*CALL f2\(\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*\d+:\s*f1\(\);
-^\s*\d+:\s*f3\(\);
-^\s*\d+:\s*f4\(\);
-^\s*\d+:\s*f5\(\);
-^\s*\d+:\s*f6\(\);
-^\s*\d+:\s*f7\(\);
-^\s*\d+:\s*f8\(\);
-^\s*\d+:\s*f9\(\);
+^\s*\d+:\s*CALL f1\(\)
+^\s*\d+:\s*CALL f3\(\)
+^\s*\d+:\s*CALL f4\(\)
+^\s*\d+:\s*CALL f5\(\)
+^\s*\d+:\s*CALL f6\(\)
+^\s*\d+:\s*CALL f7\(\)
+^\s*\d+:\s*CALL f8\(\)
+^\s*\d+:\s*CALL f9\(\)
 --
 Though this example program appears to lose const-ness, since it is a primitive
 it is a copy so it is irrelevant.
diff --git a/regression/goto-analyzer/precise-const-fp/test.desc b/regression/goto-analyzer/precise-const-fp/test.desc
index 791dbe0703c..f6359140fef 100644
--- a/regression/goto-analyzer/precise-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f2\(\);
+^\s*CALL f2\(\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc
index 479c26e4afe..a5e81889688 100644
--- a/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-pointer-const-struct-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f2\(\);$
+^\s*CALL f2\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc
index 791dbe0703c..f6359140fef 100644
--- a/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-const-struct-non-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f2\(\);
+^\s*CALL f2\(\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-derefence-const-pointer-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-derefence/test.desc b/regression/goto-analyzer/precise-derefence/test.desc
index 791dbe0703c..f6359140fef 100644
--- a/regression/goto-analyzer/precise-derefence/test.desc
+++ b/regression/goto-analyzer/precise-derefence/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f2\(\);
+^\s*CALL f2\(\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-dereference-address-pointer-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-dereference-const-struct-const-pointer-const-struct-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc
index 02bf70c4391..59a16b0d748 100644
--- a/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc
+++ b/regression/goto-analyzer/precise-dereference-const-struct-pointer-const-fp/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*f3\(\);$
+^\s*CALL f3\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/regenerate-entry-function/test.desc b/regression/goto-analyzer/regenerate-entry-function/test.desc
index ecc9f85a199..6d810517674 100644
--- a/regression/goto-analyzer/regenerate-entry-function/test.desc
+++ b/regression/goto-analyzer/regenerate-entry-function/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --function fun --show-goto-functions
-^\s*fun\(x\);$
+^\s*CALL fun\(.*::x\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc b/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc
index 830458c1c3f..b87d694580e 100644
--- a/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc
+++ b/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc
@@ -6,7 +6,7 @@ CORE
 "sourceLocation":
 "function": "not_called",
 "line": "5",
-"statement": "not_called#return_value = x \+ x;"
+"statement": "ASSIGN not_called#return_value := .*x \+ .*x"
 "sourceLocation":
 "function": "not_called",
 "line": "5",
@@ -16,7 +16,7 @@ CORE
 "sourceLocation":
 "function": "dead_inside",
 "line": "12",
-"statement": "y = y \+ 1;"
+"statement": "ASSIGN .*::y := .*::y \+ 1"
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc b/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc
index c71ba15f5c9..00a9b7d50e8 100644
--- a/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc
+++ b/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc
@@ -5,11 +5,11 @@ unreachable.c
 ^SIGNAL=0$
 not_called
 // 28 file unreachable.c line 5 function not_called$
-not_called#return_value = x \+ x;$
+not_called#return_value := .*::x \+ .*::x$
 // 29 file unreachable.c line 5 function not_called$
 GOTO 1$
 dead_inside
 // 34 file unreachable.c line 12 function dead_inside$
-y = y \+ 1;$
+y := .*::y \+ 1$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc b/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc
index fd3ce8b0c91..e7c3e0888ce 100644
--- a/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc
+++ b/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc
@@ -5,14 +5,14 @@ CORE
 ^SIGNAL=0$
 not_called
 // 28 file unreachable.c line 5 function not_called$
-not_called#return_value = x \+ x;$
+not_called#return_value := .*::x \+ .*::x$
 // 29 file unreachable.c line 5 function not_called$
 GOTO 1$
 dead_inside
 // 34 file unreachable.c line 12 function dead_inside$
-y = y \+ 1;$
+y := .*::y \+ 1$
 obviously_dead
 // 40 file unreachable-instructions-basic-text/unreachable.c line 20 function obviously_dead
-x = x \+ 1;
+x := .*::x \+ 1
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/variable-sensitivity-annihiliator-test/test.desc b/regression/goto-analyzer/variable-sensitivity-annihiliator-test/test.desc
index 5584947a6dc..8c7c3d455bd 100644
--- a/regression/goto-analyzer/variable-sensitivity-annihiliator-test/test.desc
+++ b/regression/goto-analyzer/variable-sensitivity-annihiliator-test/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 line 18 function func
-g_out = 1;
+g_out := 1
 line 24 function func
-g_out = 3;
+g_out := 3
 --
diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-02/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-02/test.desc
index 1f0332d5afc..61b790678ee 100644
--- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-02/test.desc
+++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-02/test.desc
@@ -4,7 +4,7 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-Control dependencies: [0-9]+ \[TRUE\]\n.*\n.*\n\s+a = 1;
-Control dependencies: [0-9]+ \[UNCONDITIONAL\]\n.*\n.*\n\s+a = 2;
+Control dependencies: [0-9]+ \[TRUE\]\n.*\n.*\n\s+ASSIGN .*a := 1
+Control dependencies: [0-9]+ \[UNCONDITIONAL\]\n.*\n.*\n\s+ASSIGN .*a := 2
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph15/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph15/test.desc
index 6217396b36b..9c4f3a823d8 100644
--- a/regression/goto-analyzer/variable-sensitivity-dependence-graph15/test.desc
+++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph15/test.desc
@@ -4,8 +4,8 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-Control dependencies: [0-9]+ \[UNCONDITIONAL\]\n(.*\n){2,3}.*g_out2 = t1;
-Control dependencies: [0-9]+ \[TRUE\]\n(.*\n){2,3}.*g_out1 = t2;
-Control dependencies: [0-9]+ \[FALSE\]\n(.*\n){2,3}.*g_out1 = 0;
+Control dependencies: [0-9]+ \[UNCONDITIONAL\]\n(.*\n){2,3}.*g_out2 := .*t1
+Control dependencies: [0-9]+ \[TRUE\]\n(.*\n){2,3}.*g_out1 := .*t2
+Control dependencies: [0-9]+ \[FALSE\]\n(.*\n){2,3}.*g_out1 := 0
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc
index d9c98288288..1132fa4e2c1 100644
--- a/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc
+++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph16/test.desc
@@ -6,5 +6,5 @@ activate-multi-line-match
 ^SIGNAL=0$
 // Assignment from the result of a function call to a function with no body
 // should have a data dependency on the function
-^Data dependencies: 3 \[f2\]\n(.*\n).*\/\/ 4 file .*main.c line 15 function main\n.*t2 = NONDET\([^)]*\);
+^Data dependencies: 3 \[f2\]\n(.*\n).*\/\/ 4 file .*main.c line 15 function main\n.*t2 := .*nondet.*
 --
diff --git a/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc b/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc
index 40cb3664871..68b40c1af3a 100644
--- a/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc
+++ b/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 '--function fun --show-goto-functions'
-^\s*fun\(x\);$
+^\s*CALL fun\(.*::x\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-harness/array-types/test.desc b/regression/goto-harness/array-types/test.desc
index e27b1735f72..1585a54f583 100644
--- a/regression/goto-harness/array-types/test.desc
+++ b/regression/goto-harness/array-types/test.desc
@@ -4,7 +4,7 @@ example.c
 VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$
-type_constructor_ptr_int\(0, &arr, \(signed int \*\)\(void \*\)0\);
+CALL type_constructor_ptr_int\(0, address_of.*::arr\), .*0.*\)
 --
 incompatible pointer types
 --
diff --git a/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc b/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc
index 1cbd689c4b8..1ca7d58db7b 100644
--- a/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc
+++ b/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc
@@ -1,16 +1,16 @@
 CORE
 main.c
 --pointer-check --remove-const-function-pointers
-^\s*IF fp_tbl\[.*i\] == f2 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f3 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f4 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f4\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
-^\s*IF fp_tbl\[.*i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$
 ^warning: ignoring
diff --git a/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc
index 3669d114ae0..196c7328eeb 100644
--- a/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc
+++ b/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc
@@ -1,16 +1,16 @@
 CORE
 main.c
 --pointer-check --remove-function-pointers
-^\s*IF fp_tbl\[.*i\] == f2 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f3 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f4 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f4\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
-^\s*IF fp_tbl\[.*i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[.*i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF fp_tbl\[.*i.*\] = address_of\(f9\) THEN GOTO [0-9]$
 ^warning: ignoring
diff --git a/regression/goto-instrument/fp-reachability-slice1/test.desc b/regression/goto-instrument/fp-reachability-slice1/test.desc
index 803f790ee84..5c7b08aa83f 100644
--- a/regression/goto-instrument/fp-reachability-slice1/test.desc
+++ b/regression/goto-instrument/fp-reachability-slice1/test.desc
@@ -3,9 +3,9 @@ main.c
 --fp-reachability-slice c
 ^EXIT=0$
 ^SIGNAL=0$
-1: ASSUME FALSE
-dead e;
-dead d;
+1: ASSUME false
+DEAD .*::e
+DEAD .*::d
 --
 ^warning: ignoring
-dead f;
+DEAD .*::f
diff --git a/regression/goto-instrument/fp-reachability-slice2/test.desc b/regression/goto-instrument/fp-reachability-slice2/test.desc
index 36f6ee8dafc..f593c6822d5 100644
--- a/regression/goto-instrument/fp-reachability-slice2/test.desc
+++ b/regression/goto-instrument/fp-reachability-slice2/test.desc
@@ -3,8 +3,8 @@ main.c
 --fp-reachability-slice a,c
 ^EXIT=0$
 ^SIGNAL=0$
-dead d;
-dead e;
+DEAD .*::d
+DEAD .*::e
 --
 ^warning: ignoring
-dead f;
+DEAD .*::f
diff --git a/regression/goto-instrument/gcc_attribute_used1/test.desc b/regression/goto-instrument/gcc_attribute_used1/test.desc
index 99890290f0e..ef8311e5230 100644
--- a/regression/goto-instrument/gcc_attribute_used1/test.desc
+++ b/regression/goto-instrument/gcc_attribute_used1/test.desc
@@ -3,7 +3,7 @@ main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^[[:space:]]*foo = 42;$
+^[[:space:]]*ASSIGN foo := 42$
 --
 ^warning: ignoring
 ^CONVERSION ERROR$
diff --git a/regression/goto-instrument/inline_02/test.desc b/regression/goto-instrument/inline_02/test.desc
index 20e93e09f77..5dd60ae89a6 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 3b6645c8a4c..2277e6cee3c 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 8f2f03cf5f3..49195dfa496 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_08/test.desc b/regression/goto-instrument/inline_08/test.desc
index 63e8a494a30..b866f33be66 100644
--- a/regression/goto-instrument/inline_08/test.desc
+++ b/regression/goto-instrument/inline_08/test.desc
@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-y = 1;
-y = 2;
-y = 3;
+y := 1
+y := 2
+y := 3
 --
 ^warning: ignoring
diff --git a/regression/goto-instrument/inline_09/test.desc b/regression/goto-instrument/inline_09/test.desc
index 5bb9b6b5e91..2bdaae22126 100644
--- a/regression/goto-instrument/inline_09/test.desc
+++ b/regression/goto-instrument/inline_09/test.desc
@@ -4,9 +4,9 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-^\s*x;$
-^\s*c;$
-^\s*a;$
+^\s*.*::x$
+^\s*.*::c$
+^\s*.*::a$
 no body.*'f
 --
 f\(\)
diff --git a/regression/goto-instrument/is-threaded1/test.desc b/regression/goto-instrument/is-threaded1/test.desc
index 100f5087714..58a6e7b2348 100644
--- a/regression/goto-instrument/is-threaded1/test.desc
+++ b/regression/goto-instrument/is-threaded1/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-threaded
 activate-multi-line-match
-x = 2;\nIs threaded: True
+ASSIGN x := 2\nIs threaded: True
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc b/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc
index 12541b9b590..c1a5c2a90c8 100644
--- a/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc
+++ b/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --pointer-check --remove-const-function-pointers
-^\s*fp\(\);$
+^\s*CALL \*.*::fp\(\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc
index e01224edbd5..f9a3edad66b 100644
--- a/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc
+++ b/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc
@@ -1,15 +1,15 @@
 CORE
 main.c
 --pointer-check --remove-function-pointers
-^\s*IF fp == f1 THEN GOTO [0-9]$
-^\s*IF fp == f2 THEN GOTO [0-9]$
-^\s*IF fp == f3 THEN GOTO [0-9]$
-^\s*IF fp == f4 THEN GOTO [0-9]$
-^\s*IF fp == f5 THEN GOTO [0-9]$
-^\s*IF fp == f6 THEN GOTO [0-9]$
-^\s*IF fp == f7 THEN GOTO [0-9]$
-^\s*IF fp == f8 THEN GOTO [0-9]$
-^\s*IF fp == f9 THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f1\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f5\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f6\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f7\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f8\) THEN GOTO [0-9]$
+^\s*IF .*::fp = address_of\(f9\) THEN GOTO [0-9]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc b/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc
index a04500200da..4693e9cc936 100644
--- a/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc
+++ b/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --pointer-check --remove-const-function-pointers
-^\s*f2\(\);
+^\s*CALL f2\(\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc
index 381d1c41c72..c9076a57e63 100644
--- a/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc
+++ b/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --pointer-check --remove-function-pointers
-^\s*f2\(\);
+^\s*CALL f2\(\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/region-analysis-1/test.desc b/regression/goto-instrument/region-analysis-1/test.desc
index ad0a13b16e9..1e2124e2727 100644
--- a/regression/goto-instrument/region-analysis-1/test.desc
+++ b/regression/goto-instrument/region-analysis-1/test.desc
@@ -1,8 +1,8 @@
 CORE
 test.c
 --show-sese-regions
-^Region starting at \(1, [0-9]+\) IF !\(argc % 2 != 0\) THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(8, [0-9]+\) 4: SKIP$
+^Region starting at \(1, [0-9]+\) IF .*2.* THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(8, [0-9]+\) 4: SKIP$
 ^Function contains 2 single-entry, single-exit regions:$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-10/test.desc b/regression/goto-instrument/region-analysis-10/test.desc
index cd0ecbbe0a5..1d2d865f932 100644
--- a/regression/goto-instrument/region-analysis-10/test.desc
+++ b/regression/goto-instrument/region-analysis-10/test.desc
@@ -2,7 +2,7 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(6, [0-9]+\) 2: SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(10, [0-9]+\) 4: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(6, [0-9]+\) 2: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(10, [0-9]+\) 4: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-11/test.desc b/regression/goto-instrument/region-analysis-11/test.desc
index 72705c3e7e7..214c3e45004 100644
--- a/regression/goto-instrument/region-analysis-11/test.desc
+++ b/regression/goto-instrument/region-analysis-11/test.desc
@@ -2,7 +2,7 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(9, [0-9]+\) 2: SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(13, [0-9]+\) 4: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(9, [0-9]+\) 2: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(13, [0-9]+\) 4: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-12/test.desc b/regression/goto-instrument/region-analysis-12/test.desc
index d84ef86a0e4..90279660ac2 100644
--- a/regression/goto-instrument/region-analysis-12/test.desc
+++ b/regression/goto-instrument/region-analysis-12/test.desc
@@ -2,8 +2,8 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 3 single-entry, single-exit regions:$
-^Region starting at \(4, [0-9]+\) IF !\(x % 7 != 0\) THEN GOTO 2 ends at \(9, [0-9]+\) 3: GOTO 1$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 5 ends at \(14, [0-9]+\) 6: SKIP$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 4: SKIP$
+^Region starting at \(4, [0-9]+\) IF .*7.* THEN GOTO 2 ends at \(9, [0-9]+\) 3: GOTO 1$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 5 ends at \(14, [0-9]+\) 6: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(10, [0-9]+\) 4: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-13/test.desc b/regression/goto-instrument/region-analysis-13/test.desc
index e9adb5859c1..c74a00a1fbd 100644
--- a/regression/goto-instrument/region-analysis-13/test.desc
+++ b/regression/goto-instrument/region-analysis-13/test.desc
@@ -2,8 +2,8 @@ FUTURE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 3: SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$
+^Region starting at \(2, [0-9]+\) .* x := 0 ends at \(10, [0-9]+\) 3: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/region-analysis-14/test.desc b/regression/goto-instrument/region-analysis-14/test.desc
index d8b0cc462ce..ff87ce2a2e6 100644
--- a/regression/goto-instrument/region-analysis-14/test.desc
+++ b/regression/goto-instrument/region-analysis-14/test.desc
@@ -2,7 +2,7 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(5, [0-9]+\) SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 2 ends at \(9, [0-9]+\) 3: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(5, [0-9]+\) SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 2 ends at \(9, [0-9]+\) 3: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-15/test.desc b/regression/goto-instrument/region-analysis-15/test.desc
index 6c7e6d6aab1..910291e08be 100644
--- a/regression/goto-instrument/region-analysis-15/test.desc
+++ b/regression/goto-instrument/region-analysis-15/test.desc
@@ -2,7 +2,7 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(8, [0-9]+\) 2: SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(12, [0-9]+\) 4: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(8, [0-9]+\) 2: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(12, [0-9]+\) 4: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-16/test.desc b/regression/goto-instrument/region-analysis-16/test.desc
index b68f743c7f3..92d06f8055b 100644
--- a/regression/goto-instrument/region-analysis-16/test.desc
+++ b/regression/goto-instrument/region-analysis-16/test.desc
@@ -2,8 +2,8 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 3 single-entry, single-exit regions:$
-^Region starting at \(3, [0-9]+\) 1: IF !\(x % 7 != 0\) THEN GOTO 2 ends at \(8, [0-9]+\) 3: IF x < 10 THEN GOTO 1$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(13, [0-9]+\) 5: SKIP$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(9, [0-9]+\) SKIP$
+^Region starting at \(3, [0-9]+\) 1: IF .*7.* THEN GOTO 2 ends at \(8, [0-9]+\) 3: IF .*::x < 10 THEN GOTO 1$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(13, [0-9]+\) 5: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(9, [0-9]+\) SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-17/test.desc b/regression/goto-instrument/region-analysis-17/test.desc
index b101ffcd32b..2d6391f463f 100644
--- a/regression/goto-instrument/region-analysis-17/test.desc
+++ b/regression/goto-instrument/region-analysis-17/test.desc
@@ -2,8 +2,8 @@ FUTURE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 3: SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$
+^Region starting at \(2, [0-9]+\) .* x := 0 ends at \(10, [0-9]+\) 3: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/region-analysis-2/test.desc b/regression/goto-instrument/region-analysis-2/test.desc
index e6da6617df1..742fb8a1f0f 100644
--- a/regression/goto-instrument/region-analysis-2/test.desc
+++ b/regression/goto-instrument/region-analysis-2/test.desc
@@ -2,7 +2,7 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(4, [0-9]+\) IF !\(argc % 2 != 0\) THEN GOTO 1 ends at \(8, [0-9]+\) 2: SKIP$
-^Region starting at \(0, [0-9]+\) IF argc % 7 != 0 THEN GOTO 3 ends at \(11, [0-9]+\) 4: SKIP$
+^Region starting at \(4, [0-9]+\) IF .*2.* THEN GOTO 1 ends at \(8, [0-9]+\) 2: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*7.* THEN GOTO 3 ends at \(11, [0-9]+\) 4: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-3/test.desc b/regression/goto-instrument/region-analysis-3/test.desc
index 6258f57ae2b..9e47190c660 100644
--- a/regression/goto-instrument/region-analysis-3/test.desc
+++ b/regression/goto-instrument/region-analysis-3/test.desc
@@ -2,7 +2,7 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(1, [0-9]+\) IF !\(argc % 2 != 0\) THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(12, [0-9]+\) 5: END_FUNCTION$
+^Region starting at \(1, [0-9]+\) IF .*2.* THEN GOTO 1 ends at \(5, [0-9]+\) 2: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(12, [0-9]+\) 5: END_FUNCTION$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-4/test.desc b/regression/goto-instrument/region-analysis-4/test.desc
index e52001ec89a..5563acac130 100644
--- a/regression/goto-instrument/region-analysis-4/test.desc
+++ b/regression/goto-instrument/region-analysis-4/test.desc
@@ -2,7 +2,7 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(7, [0-9]+\) 2: SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(11, [0-9]+\) 4: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(7, [0-9]+\) 2: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(11, [0-9]+\) 4: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-5/test.desc b/regression/goto-instrument/region-analysis-5/test.desc
index 30440d57f54..8816462f8b8 100644
--- a/regression/goto-instrument/region-analysis-5/test.desc
+++ b/regression/goto-instrument/region-analysis-5/test.desc
@@ -2,7 +2,7 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 2: SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 3 ends at \(14, [0-9]+\) 4: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(10, [0-9]+\) 2: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 3 ends at \(14, [0-9]+\) 4: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-6/test.desc b/regression/goto-instrument/region-analysis-6/test.desc
index 642f487b5da..4eef6ebd2b2 100644
--- a/regression/goto-instrument/region-analysis-6/test.desc
+++ b/regression/goto-instrument/region-analysis-6/test.desc
@@ -2,8 +2,8 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 3 single-entry, single-exit regions:$
-^Region starting at \(4, [0-9]+\) IF x % 7 != 0 THEN GOTO 2 ends at \(8, [0-9]+\) 2: x = x \+ 1;$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(10, [0-9]+\) 3: SKIP$
+^Region starting at \(4, [0-9]+\) IF .*7.* THEN GOTO 2 ends at \(8, [0-9]+\) 2: .*x := .*x \+ 1$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(14, [0-9]+\) 5: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(10, [0-9]+\) 3: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-7/test.desc b/regression/goto-instrument/region-analysis-7/test.desc
index a4576526ea6..73a071d2a2c 100644
--- a/regression/goto-instrument/region-analysis-7/test.desc
+++ b/regression/goto-instrument/region-analysis-7/test.desc
@@ -2,6 +2,6 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 1 single-entry, single-exit regions:$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 4 ends at \(19, [0-9]+\) 6: END_FUNCTION$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 4 ends at \(19, [0-9]+\) 6: END_FUNCTION$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-8/test.desc b/regression/goto-instrument/region-analysis-8/test.desc
index 59534b3fc2a..29f3bceae7d 100644
--- a/regression/goto-instrument/region-analysis-8/test.desc
+++ b/regression/goto-instrument/region-analysis-8/test.desc
@@ -2,8 +2,8 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 3 single-entry, single-exit regions:$
-^Region starting at \(5, [0-9]+\) y = 0; ends at \(10, [0-9]+\) 3: SKIP$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 5 ends at \(18, [0-9]+\) 6: SKIP$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(14, [0-9]+\) 4: SKIP$
+^Region starting at \(5, [0-9]+\) .*::y := 0 ends at \(10, [0-9]+\) 3: SKIP$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 5 ends at \(18, [0-9]+\) 6: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(14, [0-9]+\) 4: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/region-analysis-9/test.desc b/regression/goto-instrument/region-analysis-9/test.desc
index 6ff8f290bc3..b9245004445 100644
--- a/regression/goto-instrument/region-analysis-9/test.desc
+++ b/regression/goto-instrument/region-analysis-9/test.desc
@@ -2,7 +2,7 @@ CORE
 test.c
 --show-sese-regions
 ^Function contains 2 single-entry, single-exit regions:$
-^Region starting at \(2, [0-9]+\) x = 0; ends at \(21, [0-9]+\) 6: argc = argc \+ 1;$
-^Region starting at \(0, [0-9]+\) IF !\(argc % 5 != 0\) THEN GOTO 7 ends at \(24, [0-9]+\) 8: SKIP$
+^Region starting at \(2, [0-9]+\) .*::x := 0 ends at \(21, [0-9]+\) 6: ASSIGN main::argc := main::argc \+ 1$
+^Region starting at \(0, [0-9]+\) IF .*5.* THEN GOTO 7 ends at \(24, [0-9]+\) 8: SKIP$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/remove-calls-no-body2/test.desc b/regression/goto-instrument/remove-calls-no-body2/test.desc
index 29c4bb40375..3af61ff6e61 100644
--- a/regression/goto-instrument/remove-calls-no-body2/test.desc
+++ b/regression/goto-instrument/remove-calls-no-body2/test.desc
@@ -6,9 +6,9 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 func3\(\)
 func4\(\)
-567;
-285;
-ret1.*=.*NONDET
+567\)
+285\)
+ret1 :=.*nondet.*
 --
 func1\(.*\)
 func2\(.*\)
diff --git a/regression/goto-instrument/replace-calls-01/test.desc b/regression/goto-instrument/replace-calls-01/test.desc
index 7c5582321b5..65b936d4d70 100644
--- a/regression/goto-instrument/replace-calls-01/test.desc
+++ b/regression/goto-instrument/replace-calls-01/test.desc
@@ -1,10 +1,10 @@
 CORE
 main.c
 --replace-calls f:g
-g\(0\);
+g\(0\)
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --
-f\(0\);
+f\(0\)
 ^warning: ignoring
diff --git a/regression/goto-instrument/replace-calls-02/test.desc b/regression/goto-instrument/replace-calls-02/test.desc
index a63737f5209..4023c000f62 100644
--- a/regression/goto-instrument/replace-calls-02/test.desc
+++ b/regression/goto-instrument/replace-calls-02/test.desc
@@ -1,12 +1,12 @@
 CORE
 main.c
 --replace-calls f:g --replace-calls h:i
-g\(\);
-i\(\);
+g\(\)
+i\(\)
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --
-f\(\);
-h\(\);
+f\(\)
+h\(\)
 ^warning: ignoring
diff --git a/regression/goto-instrument/show-goto-functions1/test.desc b/regression/goto-instrument/show-goto-functions1/test.desc
index 250c679543a..0aef764297b 100644
--- a/regression/goto-instrument/show-goto-functions1/test.desc
+++ b/regression/goto-instrument/show-goto-functions1/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --show-goto-functions
-HAVOC_OBJECT \(void \*\)a
+HAVOC_OBJECT .*a.*
 ^SIGNAL=0$
 ^EXIT=0$
 --
diff --git a/regression/goto-instrument/slice-global-inits1/test.desc b/regression/goto-instrument/slice-global-inits1/test.desc
index e6cfe4981f8..9096221dd35 100644
--- a/regression/goto-instrument/slice-global-inits1/test.desc
+++ b/regression/goto-instrument/slice-global-inits1/test.desc
@@ -1,13 +1,13 @@
 CORE
 main.c
 --slice-global-inits
-z = 0;$
-a =
-s2 =
+z := 0$
+a :=
+s2 :=
 ^EXIT=0$
 ^SIGNAL=0$
 --
-x = 0;$
-y = 0;$
-s1 =
+x := 0$
+y := 0$
+s1 :=
 ^warning: ignoring
diff --git a/regression/goto-instrument/slice-global-inits2/test.desc b/regression/goto-instrument/slice-global-inits2/test.desc
index 8d2e0699012..709dbe16ba3 100644
--- a/regression/goto-instrument/slice-global-inits2/test.desc
+++ b/regression/goto-instrument/slice-global-inits2/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --slice-global-inits
-x = 0;$
-y = 0;$
+x := 0$
+y := 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/slice-global-inits3/test.desc b/regression/goto-instrument/slice-global-inits3/test.desc
index 8d2e0699012..709dbe16ba3 100644
--- a/regression/goto-instrument/slice-global-inits3/test.desc
+++ b/regression/goto-instrument/slice-global-inits3/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --slice-global-inits
-x = 0;$
-y = 0;$
+x := 0$
+y := 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/splice_call_01/test.desc b/regression/goto-instrument/splice_call_01/test.desc
index 3e3233e216d..235b628f5a8 100644
--- a/regression/goto-instrument/splice_call_01/test.desc
+++ b/regression/goto-instrument/splice_call_01/test.desc
@@ -2,6 +2,6 @@ CORE
 main.c
 --splice-call main,moo
 activate-multi-line-match
-moo\(\);\n.*function main.*
+moo\(\)\n.*function main.*
 ^EXIT=0$
 ^SIGNAL=0$
\ No newline at end of file
diff --git a/regression/goto-instrument/unwind-zero-unwind3/test.desc b/regression/goto-instrument/unwind-zero-unwind3/test.desc
index 94ddc4f8e82..5091bc953ae 100644
--- a/regression/goto-instrument/unwind-zero-unwind3/test.desc
+++ b/regression/goto-instrument/unwind-zero-unwind3/test.desc
@@ -5,5 +5,5 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
-ASSUME FALSE
+ASSUME false
 ^warning: ignoring
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index 5aac7fc0b60..de9aec6ffb1 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_type.h>
 #include <util/expr_iterator.h>
 #include <util/find_symbols.h>
+#include <util/format_expr.h>
+#include <util/format_type.h>
 #include <util/invariant.h>
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
@@ -75,8 +77,7 @@ std::ostream &goto_programt::output_instruction(
   case INCOMPLETE_GOTO:
     if(!instruction.get_condition().is_true())
     {
-      out << "IF " << from_expr(ns, identifier, instruction.get_condition())
-          << " THEN ";
+      out << "IF " << format(instruction.get_condition()) << " THEN ";
     }
 
     out << "GOTO ";
@@ -103,22 +104,55 @@ std::ostream &goto_programt::output_instruction(
   case OTHER:
     if(instruction.get_other().id() == ID_code)
     {
-      const auto &code = to_code(instruction.get_other());
+      const auto &code = instruction.get_other();
       if(code.get_statement() == ID_havoc_object)
       {
-        out << "HAVOC_OBJECT " << from_expr(ns, identifier, code.op0()) << '\n';
+        out << "HAVOC_OBJECT " << format(code.op0()) << '\n';
         break;
       }
       // fallthrough
     }
-    // fallthrough
+    out << "OTHER " << format(instruction.get_other());
+    break;
 
   case RETURN:
+    out << "RETURN " << format(instruction.return_value()) << '\n';
+    break;
+
   case DECL:
+    out << "DECL " << format(instruction.decl_symbol()) << " : "
+        << format(instruction.decl_symbol().type()) << '\n';
+    break;
+
   case DEAD:
+    out << "DEAD " << format(instruction.dead_symbol()) << '\n';
+    break;
+
   case FUNCTION_CALL:
+    out << "CALL ";
+    {
+      auto &call = instruction.get_function_call();
+      if(call.lhs().is_not_nil())
+        out << format(call.lhs()) << " := ";
+      out << format(call.function());
+      out << '(';
+      bool first = true;
+      for(const auto &argument : call.arguments())
+      {
+        if(first)
+          first = false;
+        else
+          out << ", ";
+        out << format(argument);
+      }
+      out << ')';
+      out << '\n';
+    }
+    break;
+
   case ASSIGN:
-    out << from_expr(ns, identifier, instruction.get_code()) << '\n';
+    out << "ASSIGN " << format(instruction.assign_lhs())
+        << " := " << format(instruction.assign_rhs()) << '\n';
     break;
 
   case ASSUME:
@@ -129,7 +163,7 @@ std::ostream &goto_programt::output_instruction(
       out << "ASSERT ";
 
     {
-      out << from_expr(ns, identifier, instruction.get_condition());
+      out << format(instruction.get_condition());
 
       const irep_idt &comment=instruction.source_location.get_comment();
       if(!comment.empty())
@@ -163,7 +197,7 @@ std::ostream &goto_programt::output_instruction(
     }
 
     if(instruction.get_code().operands().size() == 1)
-      out << ": " << from_expr(ns, identifier, instruction.get_code().op0());
+      out << ": " << format(instruction.get_code().op0());
 
     out << '\n';
     break;
@@ -173,11 +207,8 @@ std::ostream &goto_programt::output_instruction(
     if(instruction.get_code().get_statement() == ID_exception_landingpad)
     {
       const auto &landingpad = to_code_landingpad(instruction.get_code());
-      out << "EXCEPTION LANDING PAD ("
-          << from_type(ns, identifier, landingpad.catch_expr().type())
-          << ' '
-          << from_expr(ns, identifier, landingpad.catch_expr())
-          << ")";
+      out << "EXCEPTION LANDING PAD (" << format(landingpad.catch_expr().type())
+          << ' ' << format(landingpad.catch_expr()) << ")";
     }
     else if(instruction.get_code().get_statement() == ID_push_catch)
     {