Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
c51200a4
Commit
c51200a4
authored
Jan 03, 2017
by
Guillaume Melquiond
Browse files
Bugfix: transformation split unsound due to careless closure
parent
f3bcd139
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/transform/split_goal.ml
View file @
c51200a4
...
...
@@ -225,7 +225,8 @@ let rec split_core sp f =
let
close
=
iclose
(
case
f2
sf2
.
fwd
sf2
.
neg
)
in
let
lside
=
if
sp
.
side_split
then
close
sf1
.
pos
else
!+
(
t_implies
sf2
.
fwd
sf1
.
bwd
)
in
ret
sf2
.
pos
sf1
.
neg
sf2
.
bwd
sf1
.
fwd
(
sf2
.
side
++
lside
++
close
sf1
.
side
)
let
side
=
sf2
.
side
++
lside
++
sf1
.
side
in
ret
sf2
.
pos
sf1
.
neg
sf2
.
bwd
sf1
.
fwd
side
|
Tbinop
(
Timplies
,
f1
,
f2
)
->
let
(
>->
)
=
alias2
f1
f2
t_implies
in
let
sf1
=
rc
f1
and
sf2
=
rc
f2
in
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment