jofleish
1ee3de5409
temporary workaround for build
2022-03-23 12:25:31 -04:00
jofleish
d9e93d5f7c
revert to buildid in version number
2022-03-23 09:53:15 -04:00
jofleish
13a33a3966
fix authentication input
2022-03-23 08:51:20 -04:00
jofleish
16f47954c0
Use camel case service name
2022-03-23 08:50:14 -04:00
jofleish
7bf2df1b7a
Update nightly nuget service connection
2022-03-23 08:44:42 -04:00
jofleish
8273a20498
test publish to public project feed
2022-03-22 17:26:12 -04:00
John Fleisher
ce04c16a6f
Jfleisher/nightlynuget ( #5916 )
...
* WiP: Test nightly version number change
* Fix debug assert
* WiP: test nuget publish to AzDo feed for nightly build
* WiP: Make Nuget deploy separate stage
* WiP: fix nightly stage name
* change nuget push to vstsfeed
* Try case sensitive name for artifacts
* WiP: use artifact folder names
* add Rev version to package
* WiP: build def variation on nightly build version
* WiP: use Build_BuildNumber and Build_DefinitionName
* WiP: using hyphen in nightly version
* Tag nightly packages with datetime
* fix commit
* Build.BuildId and Build.DefinitionName
* WiP: change suffix format to lead with alpha
* test z3public feed publish
* revert public publish test
* WiP: test build# versioning scheme
* WiP: another variant on version number for nightly
Co-authored-by: jfleisher <jofleish@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-22 12:19:58 -07:00
Nikolaj Bjorner
815c971c9a
#5778
...
regression when tracking literal explanations
2022-03-22 01:55:43 -07:00
Nikolaj Bjorner
4b1419261f
#5778
2022-03-21 16:23:43 -07:00
Nikolaj Bjorner
9011100df2
Update .gitignore
2022-03-21 15:25:35 -07:00
Nikolaj Bjorner
20bd59bb20
#5778 - missed tracking literal assignment justification
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-21 10:15:00 -07:00
Nikolaj Bjorner
00608cd719
notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 14:38:59 -07:00
Nikolaj Bjorner
a418678cd4
increment version number
2022-03-20 14:34:34 -07:00
Nikolaj Bjorner
f1806d32d6
remove buggy code, close, fix #5825
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 13:25:44 -07:00
Nikolaj Bjorner
1e8bae01e9
enable pypi in release pipeline
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 13:12:29 -07:00
Nikolaj Bjorner
b4873d226c
fix #5907
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 11:40:19 -07:00
Nikolaj Bjorner
f053daa051
fix #5906
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-20 11:24:42 -07:00
Nikolaj Bjorner
bbb27775ed
ensure that objects in callback are of sort Ast.
2022-03-20 11:24:42 -07:00
Chaoqi Zhang
3439d2407b
Revert "doc: update readme ( #5898 )" ( #5905 )
...
This reverts commit 313b87f3c6
.
2022-03-20 11:21:11 -07:00
Nikolaj Bjorner
9061ca58f1
call it macOSBuild
2022-03-19 15:25:50 -07:00
Nikolaj Bjorner
b5b9c85c40
call it UbuntuBuild
2022-03-19 15:24:53 -07:00
Nikolaj Bjorner
dfa65443e9
fix name for artifact
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-19 13:51:58 -07:00
Nikolaj Bjorner
964e513353
re-add bv_eq_axioms, fix #5842
2022-03-19 12:37:01 -07:00
Nikolaj Bjorner
cfe02edda5
remove stale return
2022-03-19 12:26:48 -07:00
Nikolaj Bjorner
fd1f5cdd0f
fix callback type declarations for propagators
2022-03-19 12:24:46 -07:00
Nikolaj Bjorner
eaa2fb76ca
update release pipeline with x86 Nuget
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-19 11:46:27 -07:00
Nikolaj Bjorner
86af723db7
remove left-over debug output
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-19 09:40:29 -07:00
Nikolaj Bjorner
6d836e7e2f
expose model update
2022-03-19 09:23:08 -07:00
Nikolaj Bjorner
a9d7026724
add note about transform
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 19:13:35 -07:00
Nikolaj Bjorner
81a5e56c89
publish to github
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 18:58:27 -07:00
Nikolaj Bjorner
39df8ee372
update win build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 17:39:58 -07:00
Nikolaj Bjorner
669a1d63da
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 16:36:16 -07:00
Nikolaj Bjorner
29e288367e
pre-release pipeline
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 16:22:48 -07:00
Nikolaj Bjorner
6010d751ed
fix #5903
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-18 16:21:47 -07:00
Nikolaj Bjorner
41d1c34067
remove else case
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-17 12:33:15 -07:00
Nikolaj Bjorner
1fa373d6c2
old bug: unit of xor is false
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-17 08:21:22 -07:00
Matt Thornton
4e0a2f5968
Dispose of intermediate Z3Objects created in dotnet api. ( #5901 )
...
* Dispose of intermediate Z3Objects created in dotnet api.
* Set C# LangVersion to 8.0.
* Fix build errors.
* Fix warning about empty using statement.
* Fix Xor to only dispose of objects that it creates internally.
2022-03-17 08:08:05 -07:00
Jan Vraný
bdf7de1703
Care for root index being undefine while calling Z3_algebraic_get_i() ( #5888 )
...
In some cases, Z3_algebraic_get_i() returned 0. For example, in the following
Python snippet, the last assert would fail:
import z3
x = z3.Real('x')
s = z3.Solver()
s.add( (x * x) - 2 == 0, x <= 0)
s.check()
val_x = s.model().get_interp(x)
assert val_x.index() == 1
The problem was that `algebraic_numbers::manager:👿 :get_i()` did not
check whether the root index was properly initialized.
This commit fixes this issue by checking whether root index is initialized
the same way various other routines do.
Fixes issue #5807 .
Signed-off-by: Jan Vrany <jan.vrany@labware.com>
2022-03-16 19:28:03 -07:00
Nikolaj Bjorner
6455ae4350
Merge branch 'master' of https://github.com/z3prover/z3
2022-03-16 16:30:08 -07:00
Nikolaj Bjorner
0b230ee703
move some functions to using var pattern #5900
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-16 16:29:54 -07:00
Nikolaj Bjorner
6c4780a845
Update cross-build.yml
2022-03-16 07:32:05 -07:00
Han Gao
3d87d86c28
github action: add riscv64/aarch64/powerpc64 cross compile ( #5897 )
...
* github action: add riscv64/aarch64/powerpc64 cross compile
Signed-off-by: Han Gao <rabenda.cn@gmail.com>
* fix: build on non-x86 platform
Signed-off-by: Revy <rabenda.cn@gmail.com>
2022-03-16 07:30:20 -07:00
Nikolaj Bjorner
a1517251dd
call dispose on sorts #5900 , missing charSort
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-16 07:28:05 -07:00
Nikolaj Bjorner
cd5e114ed3
call dispose on sorts #5900
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-16 07:24:33 -07:00
Nikolaj Bjorner
cb9dcb799f
add regex power to API and for Java per request
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-16 06:17:31 -07:00
Nikolaj Bjorner
e1929ca9b9
add regex power to API and for Java per request
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-15 19:18:33 -07:00
Nikolaj Bjorner
706d7ea893
native context uses legacy mk_context
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-03-15 16:01:05 -07:00
Chaoqi Zhang
313b87f3c6
doc: update readme ( #5898 )
...
add the command to `mkdir build` first
2022-03-14 09:30:08 -07:00
Nikolaj Bjorner
545341e699
fix #5895
2022-03-12 09:17:13 -08:00
Nikolaj Bjorner
c51ca86203
add another constant folding case
2022-03-10 17:39:40 -08:00