Leonardo de Moura
|
cadd35bf7a
|
checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 21:44:35 -07:00 |
|
Leonardo de Moura
|
adb6d05805
|
fixed typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 14:43:02 -07:00 |
|
Leonardo de Moura
|
398f1b1de1
|
moving assertion_stack to mcsat branch
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 13:29:09 -07:00 |
|
Leonardo de Moura
|
c096fb534b
|
checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 13:28:10 -07:00 |
|
Nikolaj Bjorner
|
4f2b7049ab
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2012-11-01 13:06:16 -07:00 |
|
Nikolaj Bjorner
|
1c17e40fe5
|
optmizing DL
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2012-11-01 13:06:10 -07:00 |
|
Leonardo de Moura
|
ef0ee9a0c4
|
code reorg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 12:47:24 -07:00 |
|
Leonardo de Moura
|
26ffee95fc
|
resurrecting assertion stack
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 12:37:24 -07:00 |
|
Leonardo de Moura
|
c9722a1313
|
removing dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 12:21:14 -07:00 |
|
Leonardo de Moura
|
f1c9c9b7cd
|
resurrecting assertion_stack
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 12:15:45 -07:00 |
|
Leonardo de Moura
|
4c98b567e1
|
old_params ==> front_end_params. Isolated abstract solver interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 11:28:14 -07:00 |
|
Leonardo de Moura
|
62cc752fb6
|
Fixed bug reported by Arie Gurfinkel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 10:28:26 -07:00 |
|
Leonardo de Moura
|
7cdf5e493b
|
moved smt tactic to smt folder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 08:48:54 -07:00 |
|
Leonardo de Moura
|
81df5ca96f
|
Moved dead code to dead branch
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-11-01 08:40:20 -07:00 |
|
Nikolaj Bjorner
|
8f7494cb04
|
disable buggy code in slicer: it removes conjuncts for non-sliced variables. It should use the same criteria as the slice recognizer. reported by Arie Gurfinkel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2012-10-31 20:29:28 -07:00 |
|
Leonardo de Moura
|
e2f3f9abd7
|
removed dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 14:58:21 -07:00 |
|
Leonardo de Moura
|
9072d80995
|
fixed typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 14:36:18 -07:00 |
|
Leonardo de Moura
|
6d8b8a762c
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2012-10-31 14:22:00 -07:00 |
|
Leonardo de Moura
|
1ebfcfc2cb
|
removing fat
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 14:21:22 -07:00 |
|
Nikolaj Bjorner
|
0b8e77aa57
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2012-10-31 13:35:45 -07:00 |
|
Nikolaj Bjorner
|
9748b6ed11
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2012-10-31 13:25:42 -07:00 |
|
Leonardo de Moura
|
a274cac2a0
|
bindings --> api; and moved nlsat/sat/subpaving tactics
|
2012-10-31 13:25:36 -07:00 |
|
Nikolaj Bjorner
|
c4cb66bbfa
|
fix bugs in inliner and usage of unbound variable fix, reported by Arie Gurfinkel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2012-10-31 13:23:24 -07:00 |
|
Leonardo de Moura
|
ccdb253b47
|
added add_extra_exe command to build framework
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 13:14:37 -07:00 |
|
Leonardo de Moura
|
7cea9cdefe
|
enable pdb for release mode 32bit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 13:09:05 -07:00 |
|
Leonardo de Moura
|
81193fd550
|
add default template instance
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 11:16:43 -07:00 |
|
Leonardo de Moura
|
92eb2ec802
|
missing update
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 11:02:14 -07:00 |
|
Leonardo de Moura
|
683687b153
|
more cleanup
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 10:54:59 -07:00 |
|
Nikolaj Bjorner
|
bdc28762d3
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2012-10-31 10:37:10 -07:00 |
|
Nikolaj Bjorner
|
832ade3ac8
|
local changes
|
2012-10-31 10:37:05 -07:00 |
|
Leonardo de Moura
|
c2e95bb0c5
|
make front_end_params an optional argument in cmd_context
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 09:43:46 -07:00 |
|
Leonardo de Moura
|
bef9390142
|
Fixed warnings reported by gcc 4.7.1
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 00:16:26 -07:00 |
|
Leonardo de Moura
|
ffcb9741dc
|
Fixed warnings reported by gcc 4.7.1
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-31 00:05:38 -07:00 |
|
Leonardo de Moura
|
0f3cba350e
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2012-10-30 23:48:23 -07:00 |
|
Leonardo de Moura
|
d8f627c6c8
|
Fixed warnings produced by gcc 4.6.3 when compiling in debug mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-30 23:43:00 -07:00 |
|
Leonardo de Moura
|
5a33882746
|
added --nodotnet option to mk_make.py
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-30 17:47:37 -07:00 |
|
Leonardo de Moura
|
b1ce9f796c
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2012-10-30 16:42:36 -07:00 |
|
Leonardo de Moura
|
3a4838c6db
|
Added LICENSE.txt to win bin distrib
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-30 16:42:05 -07:00 |
|
Nikolaj Bjorner
|
f44631ce73
|
fix bugs encountered by regression tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2012-10-30 16:13:27 -07:00 |
|
Leonardo de Moura
|
ec907a4705
|
change share library search in Z3Py
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-30 15:09:12 -07:00 |
|
Leonardo de Moura
|
5060b617ab
|
include VS redist .dlls in the win dist
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-30 14:17:02 -07:00 |
|
Leonardo de Moura
|
01d784b557
|
updated README
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-30 11:29:07 -07:00 |
|
Leonardo de Moura
|
0289a58d8a
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2012-10-30 10:53:40 -07:00 |
|
Leonardo de Moura
|
42ebb2b07c
|
updated Release notes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-30 10:53:17 -07:00 |
|
Christoph M. Wintersteiger
|
4abce8e0c3
|
UFBV performance fix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2012-10-30 17:09:09 +00:00 |
|
Leonardo de Moura
|
cb8a6db51b
|
minor fixes after feedback from regression tests...
|
2012-10-30 09:20:28 -07:00 |
|
Leonardo de Moura
|
b629dd7fdd
|
fixed der tactic installation command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-30 08:38:20 -07:00 |
|
Leonardo de Moura
|
bb40f83bcb
|
breaking dependencies
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-29 20:25:20 -07:00 |
|
Leonardo de Moura
|
759504880a
|
isolated proto_model obsolete code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2012-10-29 20:15:33 -07:00 |
|
Leonardo de Moura
|
24efe18d3f
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2012-10-29 18:58:49 -07:00 |
|