Nikolaj Bjorner
|
f591e0948a
|
fix #1841
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-22 15:28:33 -08:00 |
|
Nikolaj Bjorner
|
498fa87993
|
seq rewriting fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-22 10:48:49 -08:00 |
|
Nikolaj Bjorner
|
2cc654081c
|
Merge pull request #1955 from waywardmonkeys/Z3_bool_to_bool
Switch from using Z3_bool to using bool.
|
2018-11-20 20:29:28 -08:00 |
|
Nikolaj Bjorner
|
37ef3cbeb2
|
add rc2 sample
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-20 14:32:01 -08:00 |
|
Bruce Mitchener
|
edf8ba44d1
|
Switch from using Z3_bool to using bool.
This is a continuation of the work started by using stdbool and
continued by switching from Z3_TRUE|FALSE to true|false.
|
2018-11-20 11:27:09 +07:00 |
|
Bruce Mitchener
|
56bbed173e
|
Remove usages of Z3_TRUE / Z3_FALSE.
Now that this is all using stdbool.h, we can just use true/false.
For now, we leave the aliases in place in z3_api.h.
|
2018-11-20 00:25:37 +07:00 |
|
Nikolaj Bjorner
|
a85a612bae
|
use old-fashined C for test_capi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-15 10:03:43 -08:00 |
|
Nikolaj Bjorner
|
51a0022450
|
add recfun to API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-27 11:41:18 -05:00 |
|
Nikolaj Bjorner
|
c802a0ac96
|
fix crash exposed by examples/dotnet/Program.cs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-20 14:32:59 -07:00 |
|
Nikolaj Bjorner
|
3ba2aa2672
|
regressions in examples/dotnet/Program.cs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-20 14:01:43 -07:00 |
|
Florian Pigorsch
|
326bf401b9
|
Fix some spelling errors (mostly in comments).
|
2018-10-20 17:07:41 +02:00 |
|
Nikolaj Bjorner
|
7cc6d84e6f
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-19 21:02:15 -07:00 |
|
Nikolaj Bjorner
|
694a6a26c9
|
bump version, add double access
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-19 20:20:08 -07:00 |
|
Bruce Mitchener
|
372cab2c5b
|
Fix some typos.
|
2018-10-17 22:49:39 +07:00 |
|
Bruce Mitchener
|
a76397d3b8
|
Refer to macOS rather than Mac OS / OSX.
|
2018-10-02 17:38:09 +07:00 |
|
Nikolaj Bjorner
|
2b35f1a924
|
quip
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-16 13:14:41 -07:00 |
|
Nikolaj Bjorner
|
98dfd82765
|
adding quipie
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-15 21:55:49 -07:00 |
|
Nikolaj Bjorner
|
0232383191
|
mini IC3 sample
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-15 16:59:06 -07:00 |
|
Nikolaj Bjorner
|
94ffa3963e
|
fix #1800 by converting large integers to strings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-08-24 16:54:22 +02:00 |
|
rainoftime
|
bb534f6103
|
Add example of using z3's model construction C++ API
|
2018-07-10 11:16:20 +08:00 |
|
Nikolaj Bjorner
|
adb9a1c797
|
fix c
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-04 17:31:26 -07:00 |
|
Nikolaj Bjorner
|
03ed33ac02
|
merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-02 15:31:26 -07:00 |
|
Nikolaj Bjorner
|
648a531950
|
update java example to bypass bit-rot
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-02 09:50:29 -07:00 |
|
Nikolaj Bjorner
|
46ea054784
|
merge get_value and get_ivalue that produced different results
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-07-02 03:55:40 -07:00 |
|
Nikolaj Bjorner
|
9f3da32a77
|
remove interpolation from test_capi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-24 16:28:23 -07:00 |
|
Nikolaj Bjorner
|
50c93d1ad4
|
merge with 4.7.1
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-22 17:10:36 -07:00 |
|
Joran Honig
|
e32dfad81e
|
Add comments
|
2018-05-19 11:16:20 +02:00 |
|
Joran Honig
|
7d51353b8b
|
Implement parallel python example
|
2018-05-19 11:13:53 +02:00 |
|
Nikolaj Bjorner
|
2aedaf315a
|
fix removal bug, tune all-interval usage
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-09 16:32:38 +01:00 |
|
Nikolaj Bjorner
|
3736c0ae8b
|
touch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-03 08:52:25 -07:00 |
|
Nikolaj Bjorner
|
8ecff9e5ee
|
fix java
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-03 08:04:10 -07:00 |
|
Nikolaj Bjorner
|
e98c808f47
|
fixing compilation errors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-03 03:18:29 -07:00 |
|
Nikolaj Bjorner
|
bb041495e3
|
fix java
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-02 14:00:37 -07:00 |
|
Nikolaj Bjorner
|
14d780fb2b
|
fix dotnet example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-02 13:21:42 -07:00 |
|
Nikolaj Bjorner
|
9e59bba80e
|
fix dotnet example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-02 13:20:51 -07:00 |
|
Nikolaj Bjorner
|
ef6339f14c
|
fix build issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-01 12:00:03 -07:00 |
|
Nikolaj Bjorner
|
fa93bc419d
|
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-05-01 10:53:36 -07:00 |
|
Nikolaj Bjorner
|
f525f43e43
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-30 09:30:43 -07:00 |
|
Nikolaj Bjorner
|
3b78bdc8e5
|
shorthands in enode to access args and partents
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-06 14:01:09 -07:00 |
|
Nikolaj Bjorner
|
5ba939ad5e
|
add tuple shortcut and example to C++ API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-04-03 12:40:18 -07:00 |
|
Nikolaj Bjorner
|
32c9af5e5a
|
fix use of Z3_bool -> Z3_lbool
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-27 16:16:25 -07:00 |
|
Nikolaj Bjorner
|
c513f3ca09
|
merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-25 14:57:01 -07:00 |
|
Nikolaj Bjorner
|
0ce2001449
|
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-03-10 11:39:22 -08:00 |
|
Bruce Mitchener
|
73b3da37d8
|
Typo fixes.
|
2018-01-02 22:48:06 +07:00 |
|
Nikolaj Bjorner
|
6b258578f9
|
fix uninitialized variable m_gc_burst in config, have cuber accept and receive optional vector of variables indicating splits and global autarky as output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-14 02:38:45 -08:00 |
|
Dan Liew
|
92059942e6
|
[CMake] Use C++11 when building C++ API example.
This is a change requested by @NikolajBjorner (
5f8c97532c (commitcomment-26049417)
).
|
2017-12-07 10:56:44 +00:00 |
|
Nikolaj Bjorner
|
60af4a5820
|
deal with ambiguity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-04 19:12:51 +05:30 |
|
Nikolaj Bjorner
|
0bfea99cff
|
fix issues found in parsing examples
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-01 14:43:52 -08:00 |
|
Nikolaj Bjorner
|
a9ebda105c
|
remove assertion that gets violated on exception path (declaration of datatypes are not getting removed)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-01 08:59:36 -08:00 |
|
Nikolaj Bjorner
|
c18d60a9c5
|
fix java
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-11-29 20:56:36 -08:00 |
|