1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 29 Aug 2009 16:35:56 +0200
Subject: [PATCH] Update for why 2.19
Patch taken from upstream SVN.
Signed-off-by: Stephane Glondu <steph@glondu.net>
---
contrib/dp/dp.ml | 18 +++++++++---------
1 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 79ffaf3..d880384 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -701,7 +701,7 @@ let file_contents f =
let timeout_sys_command cmd =
if !debug then Format.eprintf "command line: %s@." cmd;
let out = Filename.temp_file "out" "" in
- let cmd = sprintf "cpulimit %d %s > %s 2>&1" !timeout cmd out in
+ let cmd = sprintf "why-cpulimit %d %s > %s 2>&1" !timeout cmd out in
let ret = Sys.command cmd in
if !debug then
Format.eprintf "Output file %s:@.%s@." out (file_contents out);
@@ -731,12 +731,12 @@ let why_files f = String.concat " " (!prelude_files @ [f])
let call_simplify fwhy =
let cmd =
- sprintf "why --no-arrays --simplify --encoding sstrat %s" (why_files fwhy)
+ sprintf "why --simplify %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
let cmd =
- sprintf "timeout %d Simplify %s > out 2>&1 && grep -q -w Valid out"
+ sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out"
!timeout fsx
in
let out = Sys.command cmd in
@@ -747,7 +747,7 @@ let call_simplify fwhy =
r
let call_ergo fwhy =
- let cmd = sprintf "why --no-arrays --why %s" (why_files fwhy) in
+ let cmd = sprintf "why --alt-ergo %s" (why_files fwhy) in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
let ftrace = Filename.temp_file "ergo_trace" "" in
@@ -797,12 +797,12 @@ let call_zenon fwhy =
let call_yices fwhy =
let cmd =
- sprintf "why --no-arrays -smtlib --encoding sstrat %s" (why_files fwhy)
+ sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
let cmd =
- sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out"
+ sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out"
!timeout fsmt
in
let out = Sys.command cmd in
@@ -814,7 +814,7 @@ let call_yices fwhy =
let call_cvcl fwhy =
let cmd =
- sprintf "why --no-arrays --cvcl --encoding sstrat %s" (why_files fwhy)
+ sprintf "why --cvcl --encoding sstrat %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
@@ -831,7 +831,7 @@ let call_cvcl fwhy =
let call_harvey fwhy =
let cmd =
- sprintf "why --no-arrays --harvey --encoding strat %s" (why_files fwhy)
+ sprintf "why --harvey --encoding strat %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in
@@ -856,7 +856,7 @@ let call_harvey fwhy =
r
let call_gwhy fwhy =
- let cmd = sprintf "gwhy --no-arrays %s" (why_files fwhy) in
+ let cmd = sprintf "gwhy %s" (why_files fwhy) in
if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy));
NoAnswer
--
|
