projects
/
cvc5.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
history
|
raw
|
HEAD
Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report.
[cvc5.git]
/
test
/
regress
/
regress0
/
datatypes
/
tuple-record-bug.cvc
1
% EXPECT: invalid
2
3
Mem_0 : TYPE = ARRAY INT OF INT;
4
5
MEMORY : TYPE = [# int : Mem_0, queries : Mem_0 #];
6
7
x : INT;
8
9
foo : MEMORY -> MEMORY
10
= LAMBDA (x : MEMORY) : LET y = x WITH .int := x.int IN y;
11
12
m : MEMORY;
13
14
w : [MEMORY,INT] =
15
IF x = 0
16
THEN (foo(m),0)
17
ELSE (m, 0)
18
ENDIF;
19
20
QUERY w.1 = 1;