Ben Niu
962d0dda78
Pass /RELEASE to MSVC linker
...
Without /RELEASE passed to MSVC linker, the checksum field in exe/dll is not calculated. When you load the exe/dll in windbg (e.g., windbg -z libz3.dll), a warning "Unable to verify checksum" will show. With /RELEASE passed to linker, the warning will be gone.
2019-07-04 08:08:32 -07:00
Nikolaj Bjorner
6d244ed2aa
internalize reflect
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-04 07:33:37 +07:00
Nikolaj Bjorner
b86432e2a3
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-04 07:26:50 +07:00
Nikolaj Bjorner
c744b19bce
resort to only supporting ground non-linear division for nra_tactic/nra_probe #2372 #2376
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-04 07:08:47 +07:00
Nikolaj Bjorner
8e2ad4e461
#2379 and #2380
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-04 07:08:47 +07:00
Christoph M. Wintersteiger
1517ca907e
Another fix for fp.rem.
2019-07-03 16:09:07 +01:00
Christoph M. Wintersteiger
77827498bd
Added checkpoints to lia2card tactic.
2019-07-03 14:32:27 +01:00
Christoph M. Wintersteiger
df4065536f
Cleaned up FP predicates in the Python API. Fixes #2323 .
2019-07-03 12:32:28 +01:00
Christoph M. Wintersteiger
e0dc05c97e
Fixed final alignment step of fp.rem. Fixes #2369 and does not break #2289 .
2019-07-03 12:22:35 +01:00
Nikolaj Bjorner
807095a344
fix #2375
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-03 10:04:00 +07:00
Nikolaj Bjorner
1202554dbc
Merge branch 'master' of https://github.com/z3prover/z3
2019-07-02 16:16:59 +07:00
Nikolaj Bjorner
db87f2aab0
separate rewriter used by smt context from asserted formulas to avoid term substitution, exposed by #2370
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-02 15:28:21 +07:00
Nuno Lopes
60c504f4ef
make a few helpers static
2019-06-30 15:22:40 +01:00
Nikolaj Bjorner
e5dffeace4
fix #2365
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-30 08:40:41 +03:00
Nikolaj Bjorner
90098633ef
remove target from nightl'
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-30 08:36:37 +03:00
Nikolaj Bjorner
218edbe9c6
ensure also negative lt are constrained #2360
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-30 07:50:35 +03:00
Nikolaj Bjorner
85b0722df0
ensure also negative lt are constrained
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-30 07:44:06 +03:00
Nikolaj Bjorner
1f0d162b7f
fix segfault #2360
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-30 00:54:48 +03:00
Nikolaj Bjorner
6f08c0788f
put back delete step in nightly
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-29 21:00:41 +03:00
Nikolaj Bjorner
6e994f9279
temporarily disable delete
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-29 20:09:33 +03:00
Nikolaj Bjorner
8a129a3e6f
try replace for nightly to address #2362
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-28 21:23:52 -07:00
Nikolaj Bjorner
335543b374
adding comparison #2360
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-28 21:14:58 -07:00
Nikolaj Bjorner
db274ebe01
relax condition for distributing extract over ite #2359
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-23 16:48:42 -07:00
Nikolaj Bjorner
b8734273c8
pydoc regression
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-22 17:49:46 -08:00
Nikolaj Bjorner
1e21ea4645
fix cleanup bug exposed by reordering simplifcations
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-23 01:25:50 +02:00
Nikolaj Bjorner
e8080d2307
revert normalizing ordering on equality as it breaks others and doesn't necessarily lead to simplification
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-22 23:55:11 +02:00
Nikolaj Bjorner
2a1f8ac2d8
revert normalizing ordering on equality as it breaks others and doesn't necessarily lead to simplification
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-22 23:48:00 +02:00
Nikolaj Bjorner
5dfc40bf50
python regression
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 22:29:08 +02:00
Nikolaj Bjorner
b4290d4b3d
python regression
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 22:26:21 +02:00
Nikolaj Bjorner
e0a44894cf
purge smt.timeout, use timeout instead to control solver timing #2354
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 16:56:24 +02:00
Nikolaj Bjorner
63a952f254
setting ast to null on destructor to deal with #2350
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 16:40:11 +02:00
Nikolaj Bjorner
333b32b0d2
disable adding redundant ite clauses as lemma. Add as non-redundant
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 16:32:45 +02:00
Nikolaj Bjorner
cbe52e298b
remove tracing, fix doctext
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 15:08:26 +02:00
Nikolaj Bjorner
1ae0769af5
update doctest
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 11:11:37 +02:00
Nikolaj Bjorner
017680898a
update doctest
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 11:11:01 +02:00
Nikolaj Bjorner
11a8ced769
fix #2353
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 10:47:56 +02:00
Nikolaj Bjorner
89e8a1392c
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 10:40:35 +02:00
Nikolaj Bjorner
b1dbea328a
remove unreferenced
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 09:17:17 +02:00
Nikolaj Bjorner
5177cc4a9a
change lt
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-21 09:08:20 +02:00
Nikolaj Bjorner
7c9d2e0d75
pydoc test
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-20 22:44:03 +02:00
Nikolaj Bjorner
b1893f2a58
fix build issue for debug mode
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-20 17:21:04 +02:00
Nuno Lopes
1827f98851
more fixes for mutexes in shell
2019-06-19 16:42:00 +01:00
Nuno Lopes
e603bc1ea1
remove suport for VS 2013
2019-06-19 15:06:39 +01:00
Nikolaj Bjorner
88d51d3377
fix python doc regression
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-17 12:34:56 -07:00
Nikolaj Bjorner
3985cfa33c
ensure parameters are passed to local search
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-17 12:31:13 -07:00
Nikolaj Bjorner
0f7ff2a3d0
swap
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-17 10:40:09 -07:00
Nikolaj Bjorner
262acc0556
guard insertion into enode vector @Nils-Becker, produces overflow during heavy quantifier instantiation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-17 10:28:35 -07:00
Nikolaj Bjorner
f3b79087ee
add default tactic as option to overwrite the behavior of strategic solver factory
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-17 09:27:10 -07:00
Nikolaj Bjorner
1e770af1cc
local sort
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-17 07:56:38 -07:00
Nikolaj Bjorner
ec1653fdff
Merge pull request #2345 from schedutron/master
...
Fix typo in ForAll Doc
2019-06-15 01:51:24 +02:00
