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
52db5af0
Commit
52db5af0
authored
Sep 14, 2016
by
MARCHE Claude
Browse files
fixed settings of limits
parent
8a4e6770
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/session/controller_itp.ml
View file @
52db5af0
...
...
@@ -82,8 +82,7 @@ let build_prover_call c id pr limit callback =
let
(
config_pr
,
driver
)
=
Hprover
.
find
c
.
controller_provers
pr
in
let
command
=
Whyconf
.
get_complete_command
config_pr
~
with_steps
:
(
limit
.
Call_provers
.
limit_steps
<>
Call_provers
.
empty_limit
.
Call_provers
.
limit_steps
)
in
~
with_steps
:
Call_provers
.(
limit
.
limit_steps
<>
empty_limit
.
limit_steps
)
in
let
task
=
Session_itp
.
get_task
c
.
controller_session
id
in
let
call
=
Driver
.
prove_task
?
old
:
None
~
cntexample
:
false
~
inplace
:
false
~
command
...
...
src/why3shell/why3shell.ml
View file @
52db5af0
...
...
@@ -233,12 +233,7 @@ let test_schedule_proof_attempt fmt _args =
fprintf
fmt
"status: %a@."
Controller_itp
.
print_status
status
in
let
limit
=
Call_provers
.{
limit_time
=
5
;
limit_mem
=
1000
;
limit_steps
=
-
1
;
}
in
let
limit
=
Call_provers
.{
empty_limit
with
limit_time
=
2
}
in
C
.
schedule_proof_attempt
cont
id
alt_ergo
.
Whyconf
.
prover
~
limit
~
callback
...
...
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