Nikolaj Bjorner
7063ad81cc
updates
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-25 19:42:06 -07:00
Nikolaj Bjorner
a79400a01b
fix bugs in scc_tr
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-25 14:55:42 -07:00
Nikolaj Bjorner
bfc0b214ab
update script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-21 14:49:36 -07:00
Nikolaj Bjorner
12f147403c
update script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-21 14:13:27 -07:00
Nikolaj Bjorner
5d68a09233
update script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-21 11:25:38 -07:00
Nikolaj Bjorner
1470dbf517
back to path
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-21 10:57:40 -07:00
Nikolaj Bjorner
ba30365e2d
updated script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-21 10:26:09 -07:00
Nikolaj Bjorner
9765a6d0d3
updated script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-21 09:23:01 -07:00
Nikolaj Bjorner
ff2924e83b
fix mac build error
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-20 17:19:40 -07:00
Nikolaj Bjorner
6304578111
mac
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-20 17:08:26 -07:00
Nikolaj Bjorner
16d2c2c506
mac
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-20 17:06:54 -07:00
Nikolaj Bjorner
116f0e0c70
cd below
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-20 17:05:12 -07:00
Nikolaj Bjorner
971f83997c
add ls
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-20 17:02:19 -07:00
Nikolaj Bjorner
76eae5fa5c
add mac build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-20 16:57:01 -07:00
Nikolaj Bjorner
dc01266354
fixing after clone
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 20:50:24 -07:00
Nikolaj Bjorner
d5bd7878b3
fix example test
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 20:03:47 -07:00
Nikolaj Bjorner
d5811a13eb
add test-benchmarks
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 19:18:05 -07:00
Nikolaj Bjorner
b727a3463d
update vsts
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 18:21:34 -07:00
Nikolaj Bjorner
ac2fe879ae
update script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 15:55:00 -07:00
Nikolaj Bjorner
ba2e28fa0e
update build script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 14:55:38 -07:00
Nikolaj Bjorner
7ded2a90e6
remove unreachable from vector
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 11:55:18 -07:00
Nikolaj Bjorner
7a64c82d99
comment out pull
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 11:15:49 -07:00
Nikolaj Bjorner
a873cc41bf
update vsts script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 10:43:59 -07:00
Nikolaj Bjorner
8602c52bc9
fix test build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 10:41:42 -07:00
Nikolaj Bjorner
afb12fe6c3
move script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-18 17:22:58 -07:00
Nikolaj Bjorner
ad92bfb1a1
fix python build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-01 20:19:24 -08:00
Nikolaj Bjorner
fd49a0c89c
added facility to persist model transformations
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-11-02 00:05:52 -05:00
Christoph M. Wintersteiger
e50470f2c4
Added support for MSYS2
2017-10-30 18:24:38 +00:00
Nikolaj Bjorner
60b970b9ba
add proofs dependency to solver
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-28 16:23:13 -07:00
Nikolaj Bjorner
db65cc007a
move more proof utils
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-24 10:27:48 -07:00
Nikolaj Bjorner
d67f3c1466
create proofs folder, move proof-post-order utility to proofs directory, fix regression with proofs
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-24 03:08:56 -07:00
Nikolaj Bjorner
c1b243a8e3
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-07 19:24:30 +01:00
Nikolaj Bjorner
a625301a41
expose incremental cubing over API
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-09-28 15:05:10 -07:00
Christoph M. Wintersteiger
9a464dded4
Removed -std=c++11 from OCaml stubs build command. Fixes #1263 .
2017-09-27 14:22:59 +01:00
Nikolaj Bjorner
597f77cd77
initial sketch for dominator based simplifiation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-28 20:03:31 -07:00
Nicolas Braud-Santoni
4cb7f72509
First version of the inj. tactic
2017-08-22 17:10:20 +00:00
Nikolaj Bjorner
e1d08e9526
remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-17 20:41:29 -07:00
Dan Liew
a2d7b43554
Update header includes to be relative to src/
directory.
2017-08-17 18:26:53 +01:00
Nuno Lopes
4b00bc636b
revert the patch to remove no-strict-aliasing
...
VS 2012 doesnt support C++11 unions..
2017-08-14 23:00:59 +01:00
Nikolaj Bjorner
dc4dbdf51e
Merge branch 'master' of https://github.com/z3prover/z3
2017-08-14 12:52:41 -07:00
Nikolaj Bjorner
086ea7867e
another stab at #989
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-14 12:52:25 -07:00
Nuno Lopes
2473c69679
Drop no-strict-aliasing and fix 2 places where it was violated
2017-08-14 20:09:49 +01:00
Nikolaj Bjorner
5fdea2cb18
use rfind instead of index to avoid prefix clashes #534
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-03 10:19:07 -07:00
Nikolaj Bjorner
8844112418
update header include generation to use relative paths #534
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-03 08:50:04 -07:00
Nikolaj Bjorner
2b82fd5d0c
updated include directives
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-01 10:51:47 -07:00
Christoph M. Wintersteiger
6bc5209e26
Fixed build problems with .vcxproj
2017-08-01 15:53:55 +01:00
Nikolaj Bjorner
0eb2915e83
Merge pull request #1182 from agurfinkel/spacer-z3
...
Spacer
2017-07-31 17:10:09 -07:00
Nikolaj Bjorner
8fdf3177da
add initialization to unused parameters
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 14:06:29 -07:00
Arie Gurfinkel
5b9bf74787
Spacer engine for HORN logic
...
The algorithms implemented in the engine are described in the following papers
Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96
Nikolaj Bjørner, Arie Gurfinkel:
Property Directed Polyhedral Abstraction. VMCAI 2015: 263-281
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki:
SMT-Based Model Checking for Recursive Programs. CAV 2014: 17-34
2017-07-31 17:02:29 -04:00
Nikolaj Bjorner
b19f94ae5b
make include paths uniformly use path relative to src. #534
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00