Update templates (negative steps don't get scaled).

HeisenbugLtd · Jul 19, 2020 · 49d6a28 · 49d6a28
1 parent 4be1069
commit 49d6a28
Show file tree

Hide file tree

Showing 20 changed files with 800 additions and 800 deletions.
diff --git a/test/spat.test-issues.radca.template b/test/spat.test-issues.radca.template
@@ -1621,21 +1621,21 @@ RFLX.RFLX_Types.First_Bit_Index
 RFLX.RFLX_Types.Last_Bit_Index                                                                        =>                                                      0.0 s (0 steps)/0.0 s (0 steps)/0.0 s
 RFLX.RFLX_Types.U64_Extract                                                                           =>                                                      37.9 s (99104 steps)/120.0 s (99104 steps)/1.8 ks
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:131:29                                                  => 37.9 s (99104 steps)/120.0 s (99104 steps)/1.1 ks
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 37.9 s (46879 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 33.5 s (74907 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 23.4 s (99104 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 16.6 s (69076 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 14.8 s (62940 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 13.2 s (30782 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 10.9 s (45366 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 4.3 s (12920 steps), Valid
  `-Z3: 50.0 ms (1 step), Valid
  `-Z3: 30.0 ms (1 step), Valid
@@ -1662,22 +1662,22 @@ RFLX.RFLX_Types.U64_Extract
  `-Z3: 10.0 ms (1 step), Valid
  `-Z3: 10.0 ms (1 step), Valid
 `-VC_OVERFLOW_CHECK rflx-rflx_generic_types.adb:131:27                                                => 27.1 s (35021 steps)/120.0 s (35021 steps)/147.1 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 27.1 s (35021 steps), Valid
  `-Z3: 20.0 ms (1 step), Valid
 `-VC_LOOP_INVARIANT_PRESERV rflx-rflx_generic_types.adb:137:33                                        => 25.0 s (39862 steps)/120.0 s (39862 steps)/145.0 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 25.0 s (39862 steps), Valid
  `-Z3: 10.0 ms (1 step), Valid
 `-VC_OVERFLOW_CHECK rflx-rflx_generic_types.adb:147:30                                                => 24.8 s (35564 steps)/120.0 s (35564 steps)/144.8 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 24.8 s (35564 steps), Valid
 `-VC_POSTCONDITION rflx-rflx_generic_types.adb:101:9                                                  => 23.3 s (48849 steps)/120.0 s (48849 steps)/143.3 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 23.3 s (48849 steps), Valid
  `-Trivial: 0.0 s (0 steps), Valid
 `-VC_DIVISION_CHECK rflx-rflx_generic_types.adb:151:52                                                => 19.6 s (39010 steps)/120.0 s (39010 steps)/139.6 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 19.6 s (39010 steps), Valid
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:132:65                                                  => 170.0 ms (1 step)/170.0 ms (1 step)/580.0 ms
  `-Z3: 170.0 ms (1 step), Valid
@@ -1825,26 +1825,26 @@ RFLX.RFLX_Types.U64_Extract
  `-Z3: 10.0 ms (1 step), Valid
 RFLX.RFLX_Types.U64_Extract.D                                                                         =>                                                      4.7 s (308 steps)/9.5 s (308 steps)/70.6 s
 `-VC_ASSERT rflx-rflx_generic_types.adb:117:25                                                        => 4.7 s (308 steps)/9.5 s (308 steps)/14.2 s
- `-Z3: 9.5 s (1 step), Out Of Memory
+ `-Z3: 9.5 s (-1 steps), Out Of Memory
   -CVC4: 4.7 s (308 steps), Valid
 `-VC_OVERFLOW_CHECK rflx-rflx_generic_types.adb:117:41                                                => 2.1 s (1 step)/9.3 s (1 step)/11.4 s
- `-Z3: 9.3 s (1 step), Out Of Memory
+ `-Z3: 9.3 s (-1 steps), Out Of Memory
   -CVC4: 2.1 s (1 step), Valid
 `-VC_OVERFLOW_CHECK rflx-rflx_generic_types.adb:120:77                                                => 60.0 ms (1 step)/9.0 s (1 step)/9.1 s
- `-Z3: 9.0 s (1 step), Out Of Memory
+ `-Z3: 9.0 s (-1 steps), Out Of Memory
   -CVC4: 60.0 ms (1 step), Valid
 `-VC_RANGE_CHECK rflx-rflx_generic_types.adb:123:45                                                   => 70.0 ms (1 step)/9.0 s (1 step)/9.1 s
- `-Z3: 9.0 s (1 step), Out Of Memory
+ `-Z3: 9.0 s (-1 steps), Out Of Memory
   -CVC4: 70.0 ms (1 step), Valid
 `-VC_INDEX_CHECK rflx-rflx_generic_types.adb:121:43                                                   => 40.0 ms (1 step)/9.0 s (1 step)/9.0 s
- `-Z3: 9.0 s (1 step), Out Of Memory
+ `-Z3: 9.0 s (-1 steps), Out Of Memory
   -CVC4: 40.0 ms (1 step), Valid
  `-Z3: 20.0 ms (1 step), Valid
 `-VC_RANGE_CHECK rflx-rflx_generic_types.adb:123:34                                                   => 50.0 ms (1 step)/9.0 s (1 step)/9.0 s
- `-Z3: 9.0 s (1 step), Out Of Memory
+ `-Z3: 9.0 s (-1 steps), Out Of Memory
   -CVC4: 50.0 ms (1 step), Valid
 `-VC_RANGE_CHECK rflx-rflx_generic_types.adb:121:75                                                   => 40.0 ms (1 step)/8.6 s (1 step)/8.7 s
- `-Z3: 8.6 s (1 step), Out Of Memory
+ `-Z3: 8.6 s (-1 steps), Out Of Memory
   -CVC4: 40.0 ms (1 step), Valid
 `-VC_OVERFLOW_CHECK rflx-rflx_generic_types.adb:116:46                                                => 30.0 ms (1 step)/30.0 ms (1 step)/30.0 ms
  `-Z3: 30.0 ms (1 step), Valid
@@ -1873,29 +1873,29 @@ RFLX.RFLX_Types.U64_Extract.D.ES
  `-Z3: 10.0 ms (1 step), Valid
 RFLX.RFLX_Types.U64_Extract_Intermediate                                                              =>                                                      6.7 s (10674 steps)/120.0 s (10674 steps)/617.3 s
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:62:39                                                   => 6.7 s (5481 steps)/120.0 s (5481 steps)/126.8 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 6.7 s (5481 steps), Valid
  `-Z3: 30.0 ms (1 step), Valid
  `-Z3: 20.0 ms (1 step), Valid
  `-Z3: 10.0 ms (1 step), Valid
  `-Z3: 10.0 ms (1 step), Valid
  `-Trivial: 0.0 s (0 steps), Valid
 `-VC_DIVISION_CHECK rflx-rflx_generic_types.adb:62:61                                                 => 3.0 s (4713 steps)/120.0 s (4713 steps)/123.0 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 3.0 s (4713 steps), Valid
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:65:14                                                   => 1.5 s (1 step)/120.0 s (1 step)/122.0 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 1.5 s (1 step), Valid
  `-Z3: 280.0 ms (1 step), Valid
  `-Z3: 260.0 ms (1 step), Valid
  `-Z3: 20.0 ms (1 step), Valid
  `-Z3: 10.0 ms (1 step), Valid
  `-Trivial: 0.0 s (0 steps), Valid
 `-VC_OVERFLOW_CHECK rflx-rflx_generic_types.adb:58:82                                                 => 1.3 s (1 step)/120.0 s (1 step)/121.3 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 1.3 s (1 step), Valid
 `-VC_DIVISION_CHECK rflx-rflx_generic_types.adb:63:49                                                 => 40.0 ms (1 step)/120.0 s (1 step)/120.0 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 40.0 ms (1 step), Valid
 `-VC_OVERFLOW_CHECK rflx-rflx_generic_types.adb:65:34                                                 => 2.7 s (10674 steps)/2.7 s (10674 steps)/2.7 s
  `-Z3: 2.7 s (10674 steps), Valid
@@ -1926,10 +1926,10 @@ RFLX.RFLX_Types.U64_Extract_Intermediate
  `-Z3: 10.0 ms (1 step), Valid
 RFLX.RFLX_Types.U64_Extract_Remaining                                                                 =>                                                      10.1 s (25590 steps)/120.0 s (25590 steps)/376.5 s
 `-VC_OVERFLOW_CHECK rflx-rflx_generic_types.adb:85:91                                                 => 10.1 s (25590 steps)/120.0 s (25590 steps)/130.1 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 10.1 s (25590 steps), Valid
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:87:40                                                   => 3.5 s (5190 steps)/120.0 s (5190 steps)/123.6 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 3.5 s (5190 steps), Valid
  `-Z3: 20.0 ms (1 step), Valid
  `-Z3: 20.0 ms (1 step), Valid
@@ -1938,7 +1938,7 @@ RFLX.RFLX_Types.U64_Extract_Remaining
  `-Z3: 20.0 ms (1 step), Valid
  `-Trivial: 0.0 s (0 steps), Valid
 `-VC_DIVISION_CHECK rflx-rflx_generic_types.adb:87:58                                                 => 1.2 s (1826 steps)/120.0 s (1826 steps)/121.2 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 1.2 s (1826 steps), Valid
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:89:14                                                   => 90.0 ms (1 step)/90.0 ms (1 step)/360.0 ms
  `-Z3: 90.0 ms (1 step), Valid
@@ -2004,48 +2004,48 @@ RFLX.RFLX_Types.U64_Extract_Remaining
  `-Z3: 10.0 ms (1 step), Valid
 RFLX.RFLX_Types.U64_Insert                                                                            =>                                                      54.2 s (94470 steps)/120.0 s (94470 steps)/1.6 ks
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:221:39                                                  => 5.2 s (6092 steps)/120.0 s (6092 steps)/490.6 s
- `-CVC4: 120.0 s (1 step), Timeout
-  -Z3: 120.0 s (1 step), Timeout
+ `-CVC4: 120.0 s (-1 steps), Timeout
+  -Z3: 120.0 s (-1 steps), Timeout
   -altergo: 181.9 ms (3010 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 5.2 s (6092 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 5.1 s (6092 steps), Valid
  `-Z3: 60.0 ms (1 step), Valid
  `-Z3: 30.0 ms (1 step), Valid
  `-Z3: 20.0 ms (1 step), Valid
  `-Trivial: 0.0 s (0 steps), Valid
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:259:19                                                  => 5.9 s (16665 steps)/120.0 s (16665 steps)/251.9 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 5.9 s (16665 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 5.9 s (16665 steps), Valid
  `-Z3: 50.0 ms (1 step), Valid
  `-Z3: 50.0 ms (1 step), Valid
  `-Z3: 10.0 ms (1 step), Valid
  `-Z3: 10.0 ms (1 step), Valid
  `-Trivial: 0.0 s (0 steps), Valid
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:251:19                                                  => 1.6 s (4517 steps)/120.0 s (4517 steps)/243.2 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 1.6 s (4517 steps), Valid
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 1.5 s (4517 steps), Valid
  `-Z3: 30.0 ms (1 step), Valid
  `-Z3: 20.0 ms (1 step), Valid
  `-Z3: 10.0 ms (1 step), Valid
  `-Z3: 10.0 ms (1 step), Valid
  `-Trivial: 0.0 s (0 steps), Valid
 `-VC_RANGE_CHECK rflx-rflx_generic_types.adb:282:48                                                   => 297.4 ms (4075 steps)/120.0 s (4075 steps)/240.3 s
- `-CVC4: 120.0 s (1 step), Timeout
-  -Z3: 120.0 s (1 step), Timeout
+ `-CVC4: 120.0 s (-1 steps), Timeout
+  -Z3: 120.0 s (-1 steps), Timeout
   -altergo: 297.4 ms (4075 steps), Valid
  `-Z3: 20.0 ms (1 step), Valid
 `-VC_RANGE_CHECK rflx-rflx_generic_types.adb:229:59                                                   => 54.2 s (94470 steps)/120.0 s (94470 steps)/174.2 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 54.2 s (94470 steps), Valid
  `-Z3: 20.0 ms (1 step), Valid
 `-VC_PRECONDITION rflx-rflx_generic_types.adb:278:38                                                  => 26.6 s (52462 steps)/120.0 s (52462 steps)/146.7 s
- `-Z3: 120.0 s (1 step), Timeout
+ `-Z3: 120.0 s (-1 steps), Timeout
   -CVC4: 26.6 s (52462 steps), Valid
  `-Z3: 20.0 ms (1 step), Valid
  `-Z3: 20.0 ms (1 step), Valid