Nikolaj Bjorner
ee94f8f5ce
update release script
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-10 13:52:41 +01:00
Nikolaj Bjorner
5de35d46eb
fix #2390
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-10 08:55:00 +01:00
Nikolaj Bjorner
a13ac6a759
Merge pull request #2389 from agurfinkel/issue_2357
...
Uses non-flattening rewriter in profos
2019-07-10 08:54:44 +01:00
Arie Gurfinkel
7cb956a0e2
Uses non-flattening rewriter in profos
2019-07-09 13:30:11 -04:00
Nikolaj Bjorner
88aa689a70
fix #2387 , add ite-hoist rewriting, allow assumptions to be compound expressions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-09 07:40:29 +01:00
Nikolaj Bjorner
cd93cdd819
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-07-09 07:40:29 +01:00
Nuno Lopes
6bbe8e2619
add some static
2019-07-07 15:30:32 +01:00
Nikolaj Bjorner
6e63734882
Merge pull request #2368 from waywardmonkeys/fix-typo
...
Python: Fix doc comment typo.
2019-07-05 14:38:32 +07:00
Nikolaj Bjorner
164039a47c
Merge pull request #2383 from mcfi/patch-2
...
Pass /RELEASE to MSVC linker
2019-07-05 14:37:30 +07:00
Nikolaj Bjorner
dd253cdd47
Merge pull request #2382 from mcfi/patch-1
...
Remove unreferenced formal parameter name
2019-07-05 08:33:23 +07:00
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
Ben Niu
f8a9f6cce0
Remove unreferenced formal parameter name
...
MSVC reports warning C4100 when compiling z3++.h, because of unreferenced formal parameter.
2019-07-04 08:01:40 -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
Bruce Mitchener
c4e0f8ce8f
Python: Fix doc comment typo.
2019-07-01 11:52:34 +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