mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
16445 commits 23 branches 48 tags 157 MiB
Commit graph

13887 commits

Author SHA1 Message Date
Nikolaj Bjorner 5b0389615b #5780 2022-01-19 10:10:36 +01:00
Nikolaj Bjorner 06feb71eb1 fix bug in root setting exposed by incremental mode pb_solver 2022-01-18 10:55:27 +01:00
Nikolaj Bjorner 36cfb88f5f add preliminary stub to handle closure types 2022-01-17 22:01:31 -08:00
Nikolaj Bjorner d777306bb6 #5778 2022-01-17 10:43:15 -08:00
Nikolaj Bjorner fcc9f379e7 #5778 2022-01-16 19:36:00 -08:00
Nikolaj Bjorner a15da8f9ba #5778 2022-01-16 19:11:55 -08:00
Nikolaj Bjorner 637ddf9397 fix #5777 
latest issue
 2022-01-16 18:09:38 -08:00
Nikolaj Bjorner 0dd5a5e576 #5777 2022-01-16 17:46:08 -08:00
Nikolaj Bjorner a48d3fdbb1 #5777 2022-01-16 14:01:49 -08:00
Nikolaj Bjorner ea93345b75 #5777 2022-01-16 10:52:25 -08:00
Nikolaj Bjorner cd56d55e34 #5753 2022-01-16 09:31:16 -08:00
Nikolaj Bjorner bc9c6ad93d #5753 2022-01-15 18:01:31 -08:00
Nikolaj Bjorner 1b5f7cd9e5 na 2022-01-15 10:05:26 -08:00
Nikolaj Bjorner 17cfc1d034 #5753 2022-01-15 10:03:03 -08:00
Nikolaj Bjorner 74824ac901 #5753 
get_antecedent has to be well-founded. It got broken when using eval during propagation and egraph explain during conflict resolution.
 2022-01-15 09:35:25 -08:00
Nikolaj Bjorner d09abdf58e fix #5771 
Missing congruence closure enforcement on auxiliary guard predicates.
It diverges but is sound.
 2022-01-14 15:46:40 -08:00
Nikolaj Bjorner d5cc162fa7 bug in bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-13 15:42:23 -08:00
Nikolaj Bjorner 2363bfc132 internalize arithmetic sub-terms #5753 2022-01-13 15:34:04 -08:00
Nikolaj Bjorner e816946ddc handling unsimplified input 2022-01-13 14:40:46 -08:00
Nikolaj Bjorner b259f46f85 dependencies 2022-01-13 12:34:58 -08:00
Nikolaj Bjorner 4b6679e8e0 #5753 2022-01-13 12:19:54 -08:00
Nikolaj Bjorner 366cd9b16d missing pb cases 2022-01-12 14:50:40 -08:00
Nikolaj Bjorner dfe2b27f9a #5773 2022-01-12 13:28:15 -08:00
Nikolaj Bjorner 0720998bac #5753 2022-01-12 13:12:10 -08:00
Nikolaj Bjorner 10dc8d7313 #5753 2022-01-12 12:49:06 -08:00
Nikolaj Bjorner 56d3718cde add simplification with qe-lite as an option #5767 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-12 03:41:21 -08:00
Nikolaj Bjorner 08294d62e5 separate dependencies for qe_lite 2022-01-12 03:26:22 -08:00
Nikolaj Bjorner 2bcc814031 add macro to track closures declared in z3_api 
This is to ease integration with external API wrappers that rely on accessing
information about type names that are used.
#5762
 2022-01-12 02:47:39 -08:00
Nikolaj Bjorner e5eaea46aa ensure m_true is assigned #5753 2022-01-11 10:42:05 -08:00
Nikolaj Bjorner dbd5512d8c ensure enode without recursion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-11 08:35:57 -08:00
Nikolaj Bjorner 055732423c ensure enode without recursion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-11 08:35:25 -08:00
Nikolaj Bjorner 571a74c061 counting function applications #5766 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-10 14:51:25 -08:00
Nikolaj Bjorner 4cd818b578 #5766 2022-01-10 14:40:27 -08:00
Nikolaj Bjorner d3bc11dd3a bvs have to be expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-10 12:38:25 -08:00
Nikolaj Bjorner 21feefeac5 Add character access functions #5764 2022-01-10 12:33:58 -08:00
Kevin Gibbons 2b934b601d
Add WebAssembly/TypeScript bindings (#5762) 
* Add TypeScript bindings

* mark Z3_eval_smtlib2_string as async
 2022-01-09 17:16:38 -08:00
Nikolaj Bjorner f1bf660adc add case for abs (normally simplified, but not with default_tactic=smt). 2022-01-09 11:55:21 -08:00
Nikolaj Bjorner 671d071e54 #5753 2022-01-09 11:39:21 -08:00
Nikolaj Bjorner bf3c213fd3 #5753 2022-01-09 11:03:29 -08:00
Nikolaj Bjorner 90fd3d82fc enable propagation 2022-01-08 19:00:56 -08:00
Nadav Rotem 9f9543ef69
Fix unused variable warnings. (#5760) 
This commit fixes a few cases of unused variables in release builds.
The commit uses the (void)xxx; syntax which is used in other parts of
the code.
 2022-01-08 18:18:30 -08:00
Nikolaj Bjorner 36ed1ffac2 update name of artifact 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-08 15:13:46 -08:00
Nikolaj Bjorner ef481073b2 make static features avoid stack #5758 2022-01-08 11:20:18 -08:00
Nikolaj Bjorner 6013d5da47 #5755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 14:05:06 -08:00
Nikolaj Bjorner 0bc8518cb5 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 11:53:27 -08:00
Nikolaj Bjorner 199daead50 remove Z3_bool_opt #5757 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 11:52:10 -08:00
Nikolaj Bjorner 7baa4f88b0 build failure 2022-01-06 15:17:57 -08:00
Nikolaj Bjorner 2be71cfc43 #5753 2022-01-06 15:17:37 -08:00
Nikolaj Bjorner 6a3fe514f0 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-06 14:07:54 -08:00
Nikolaj Bjorner 592b1d7f65 #5752 2022-01-06 13:32:50 -08:00
Nikolaj Bjorner d14f00d61a with no last model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-06 13:02:13 -08:00
Nikolaj Bjorner dadda86bdc #5751 2022-01-06 11:43:17 -08:00
Nikolaj Bjorner 130a0c4aa0 resurrect infinitesimals from maximization function #5720 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-06 08:34:45 -08:00
Nikolaj Bjorner d7c7fbb8f1 setting roots breaks relevancy propagation 2022-01-05 21:16:25 -08:00
Nikolaj Bjorner bd8de964f7 more fixes on relevancy 2022-01-04 22:02:28 -08:00
Nikolaj Bjorner e943bee625 apply delcypher's todo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-04 20:25:14 -08:00
Nikolaj Bjorner d1fb831030 relevancy overhaul 2022-01-04 16:03:31 -08:00
Nikolaj Bjorner 4a1975053f cleanup 2022-01-03 17:37:04 -08:00
Nikolaj Bjorner 614c66f1e2 missing relevancy propagation 2022-01-03 17:21:37 -08:00
Nikolaj Bjorner fc741cf018 rename module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-03 14:23:22 -08:00
Nikolaj Bjorner a086f6218b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-03 14:15:41 -08:00
Nikolaj Bjorner a2a5924e5c purge more 2022-01-03 14:14:09 -08:00
Nikolaj Bjorner 8e3185ffe3 remove dual solver approach 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-03 14:08:01 -08:00
Nikolaj Bjorner 1f964eea90 na 2022-01-03 11:12:28 -08:00
Nikolaj Bjorner 2944449884 #5641 2022-01-03 11:12:09 -08:00
Nikolaj Bjorner cf08cdff9c #5747 2022-01-03 08:54:54 -08:00
Nikolaj Bjorner a71aa113e0 #5641 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-02 19:36:17 -08:00
Nikolaj Bjorner 9cbec3b0ca #5641 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-02 19:15:23 -08:00
Nikolaj Bjorner 43e449a805 #5641 2022-01-02 17:53:26 -08:00
Nikolaj Bjorner d0fb3cba15 #5641 - projection that skips interpreted functions can violate model evaluation. 2022-01-02 17:45:43 -08:00
Nikolaj Bjorner 0ca5e7207e #5746 2022-01-02 11:35:55 -08:00
Nikolaj Bjorner e84ddb0d9a more #5746 2022-01-02 11:33:21 -08:00
Nikolaj Bjorner 88707f37e7 Better error reporting #5746 2022-01-02 11:31:50 -08:00
Nikolaj Bjorner 543c16c73e Trace unexpected exceptions in or-else code #5746 2022-01-02 10:22:51 -08:00
Nikolaj Bjorner 5cd1fe31fd propagate parent default not add parent default) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-01 20:37:26 -08:00
Nikolaj Bjorner 8245935d41 #5641 add handlers for basic set operations to euf=true 2022-01-01 20:33:17 -08:00
Nikolaj Bjorner 9d3c8a6a2f na 2022-01-01 17:59:31 -08:00
Nikolaj Bjorner 42219204ed sketch replace_all 2022-01-01 17:39:37 -08:00
Nikolaj Bjorner 5672f5cc34 fix #5733 2022-01-01 16:40:48 -08:00
Nikolaj Bjorner 84f514a4f4 throttle ackerman on arrays 2022-01-01 15:33:33 -08:00
Nikolaj Bjorner a20b577b2f na 2022-01-01 11:26:38 -08:00
Nikolaj Bjorner ca18150c23 bypass append when src is empty 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-31 16:43:07 -08:00
Nikolaj Bjorner a44a46a514 fix #5745 2021-12-31 16:41:51 -08:00
Nikolaj Bjorner 9550321064 missed push lambdas 2021-12-31 16:33:06 -08:00
Nikolaj Bjorner 0ef0ed3b94 redoing arrays 2021-12-31 15:51:52 -08:00
Nikolaj Bjorner aa901c4e88 axiom solver improvements 2021-12-31 11:53:40 -08:00
Nikolaj Bjorner 79f0ceac4c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-30 19:13:23 -08:00
Nikolaj Bjorner fc77345bec breaking change. Enforce append semantics everywhere for parameter updates #5744 
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
 2021-12-30 19:11:14 -08:00
Nikolaj Bjorner e8833f4dac working on relevancy=3 2021-12-30 17:07:14 -08:00
Nikolaj Bjorner b87b464e69 set relevancy flag on enode 2021-12-29 17:57:28 -08:00
Nikolaj Bjorner a90b66134d make roots uniform for theory lemmas 2021-12-29 13:42:11 -08:00
Nikolaj Bjorner 69b4392210 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-29 13:04:31 -08:00
Nikolaj Bjorner f215b18e0e change registration mode for relevant_eh 2021-12-29 13:03:43 -08:00
Nikolaj Bjorner 1706f77b9e optimize propagation to only blocked literals 2021-12-28 18:53:37 -08:00
Nikolaj Bjorner 8ff8252e89 debug relevancy mode 2021-12-28 13:02:09 -08:00
Nikolaj Bjorner 743e56bda3 remove output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-28 12:08:10 -08:00
Nikolaj Bjorner 5ed27a6c38 fix initialization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-28 12:06:56 -08:00
Nikolaj Bjorner 95e26aaad9 #5742 
expose access to constructors/accessors/recognizers given datatype sort
 2021-12-28 11:00:34 -08:00
Nikolaj Bjorner 28bce8f09c working on relevant 2021-12-28 11:00:02 -08:00
Nikolaj Bjorner 9527471967 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-27 16:03:56 -08:00
Nikolaj Bjorner 6f1be09993 add direct and incremental relevancy propagator 2021-12-27 15:10:33 -08:00
Nikolaj Bjorner 42f206171d fix #5741 2021-12-27 15:10:09 -08:00
Nikolaj Bjorner d88f125818 build 2021-12-26 15:24:03 -08:00
Nikolaj Bjorner 0bd6725711 #5641 
mark all literals duplicated in dual solver as external
 2021-12-26 15:10:21 -08:00
Nikolaj Bjorner fcee2f5aa5 revert relevancy2 2021-12-26 15:10:21 -08:00
Nikolaj Bjorner 7d311ac2ef use netstandard 2.0 per recommendations 
seems that now the recommended starting point is 2.0 and not lower.
 2021-12-25 13:44:49 -08:00
Margus Veanes 5afb95b34a
improved subset checking for regexes with counters (#5731) 2021-12-22 17:53:34 -08:00
Nikolaj Bjorner 71b868d7f6 #5722 - internalize unary xnor 2021-12-22 13:32:53 -08:00
Nikolaj Bjorner 4d8bf2a874 wrong unit for xor in aig tactic #5722 2021-12-22 13:14:06 -08:00
Anton Kochkov f11fcec082
Migrate from deprecated distutils.sysconfig in scripts (#5729) 2021-12-22 07:59:13 -08:00
Anton Kochkov f3af2193d0
Use Stdlib. instead of Pervasives. due to deprecation (#5730) 2021-12-22 07:53:47 -08:00
Nikolaj Bjorner cf6486f990 bug in flatten/and/or introduced when skipping sub-expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-22 07:43:37 -08:00
Nikolaj Bjorner 4b5ee91b44 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-21 20:40:58 -08:00
Nikolaj Bjorner 09ee60ccce update comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-21 11:04:07 -08:00
zhouzhenghui 9d82c1d8a9
fix deadlock in scoped_timer destructor (#5371) 2021-12-21 18:47:13 +00:00
Nuno Lopes 94a2c91f39 fix a few compiler warnings 2021-12-21 18:30:22 +00:00
Margus Veanes 1d9aad6ea9
improved regex merging avoiding unsat nontermination (#5728) 2021-12-20 17:44:06 -08:00
Nikolaj Bjorner e0d6e04493 fix c++ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-20 16:09:39 -08:00
Nikolaj Bjorner 7a6070506d #5727 
Expose diff function,
expose allchar in Java API
expose op codes for replace/re/all
 2021-12-20 10:17:06 -08:00
Nikolaj Bjorner f01d096fb5 fix again 2021-12-20 09:51:15 -08:00
Nikolaj Bjorner ad91748b5f Merge branch 'master' of https://github.com/z3prover/z3 2021-12-20 09:21:53 -08:00
Nikolaj Bjorner 83b47f1859 fix #5726 2021-12-20 09:21:40 -08:00
Margus Veanes be38b256c8
fixed bug in is_char_const_range (#5724) 2021-12-19 17:46:42 -08:00
Margus Veanes 25d54ebb40
fixing regression of issue 1224 (#5723) 2021-12-19 14:07:53 -08:00
Nikolaj Bjorner 4b813bac1c na 2021-12-19 12:31:47 -08:00
Nikolaj Bjorner 6a039c2700 Update z3++.h 
simplify definition
 2021-12-19 11:53:01 -08:00
Margus Veanes a7b1db611c
State graph dgml update and fixes in condition simplifier (#5721) 
* improved generated dgml graph

* fixed simplification of negated ranges and did some code cleanup

* do not make loops with lower=upper=0, this is epsilon

* do not add loops with lower=upper=1

* bug fix in normalization: forgotten eps case
 2021-12-19 11:09:55 -08:00
Nikolaj Bjorner bee742111a na 2021-12-19 11:05:19 -08:00
Nikolaj Bjorner 7441bd706b na 2021-12-19 10:57:42 -08:00
Nikolaj Bjorner 85e362277c Update z3++.h 
with bindings for user propagate functions
 2021-12-18 11:56:05 -08:00
Nikolaj Bjorner f0740bdf60 move user propagte declare to context level 
declaration of user propagate functions are declared at context level instead of at solver scope.
 2021-12-18 10:56:42 -08:00
Nikolaj Bjorner 4856581b68 na 2021-12-17 16:40:19 -08:00
Nikolaj Bjorner 8ca023d541 expose propagate created 2021-12-17 16:12:47 -08:00
Nikolaj Bjorner e1ffaa7faf na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-17 11:34:57 -08:00
Nikolaj Bjorner 9c8800bdde adding a new toy for Clemens 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-17 10:45:59 -08:00
Nikolaj Bjorner 6963451704 na 2021-12-16 20:13:29 -08:00
Nikolaj Bjorner 5974200444 fixes to previous push and streamlining 2021-12-16 20:06:49 -08:00
Nikolaj Bjorner 4e82a9af5f pin expressions 2021-12-16 19:41:32 -08:00
Nikolaj Bjorner 6cc9aa3562 prepare user propagator declared functions for likely Clemens use case 2021-12-16 19:37:30 -08:00
Margus Veanes a288f9048a
Update regex union and intersection to maintain ANF (#5717) 
* added merge for unions and intersections

* added normalization rules to ensure ANF

* fixing PR comments related to merge
 2021-12-16 19:19:36 -08:00
Nikolaj Bjorner 122b0fec0f fix #5710 2021-12-16 12:30:29 -08:00
Nikolaj Bjorner a099972354 fix #5714 
It is not unlike other fuzz bugs: it exercises some behavior that applications are unlikely to expose. In this case, a rule body expanded into a conjunction with more than 1M formulas (with a lot of repetition). The original rule representation assumed silently that the number of constraints in a body would fit within 20 bits, but reality allowed bodies with as many as 2^{32} - 1 constraints.
So "minimizing" the bug as @agurfinkel asks for seems not to make too much sense.

Just running the samples in debug mode  points to the root cause.

Since fuzz bugs are not from applications and fuzz tools have the potential for creating a large number of issues, I find it reasonable to push some basic pro-active asks on filers:

- reproduce bug in debug builds to assess whether a debug assert triggers.
- minimize or keep it simpler when possible (in this case it does not apply)
- perform basic diagnostics/triage. I am basically asking to push this part of the work on to the fuzzer. Otherwise, addressing random bugs doesn't scale. Triaging should have pointed to the root cause.

Now, there tends to be something to learn from bugs. In this case, the question was: "can we avoid constraints with duplications"? In particular, it points to a basic inefficiency of extracting conjunctions (and disjunctions). The function didn't deduplicate. So I added deduplication into this function. It is used throughout z3 code base so could expose latent issues. We will see.
 2021-12-16 10:20:53 -08:00
Nikolaj Bjorner dd6a11b526 fix #5715 2021-12-16 09:35:54 -08:00
Nikolaj Bjorner 2caa7e6e45 remove EnumToNative as it drops reference counts, fixes #5713 2021-12-16 03:22:54 -08:00
Margus Veanes 2be93870c8
Cleanup regex info and some fixes in Derivative code (#5709) 
* removed unused regex info fields

* cleanup of info and fixes in antimirov derivatives

* removed extra qualification on operator
 2021-12-15 10:59:34 -08:00
Nikolaj Bjorner 3b58f548f7 remove dead code 2021-12-14 13:42:52 -08:00
Nikolaj Bjorner 03b5380a20 na 2021-12-14 13:39:52 -08:00
Nikolaj Bjorner b1d167de5b fix co-factoring' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-14 10:12:38 -08:00
Nikolaj Bjorner 5348af3c4c fix co-factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-14 10:05:09 -08:00
Nikolaj Bjorner f40becf099 remove case for non-emptiness to combine with standard membership 
as part of revising engine for addressing #5693
 2021-12-13 18:17:40 -08:00
Nikolaj Bjorner b2af7ea68f stdout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-13 15:19:29 -08:00
Nikolaj Bjorner 9ec0f94ab9 hoisting out blocker for empty 
#5693
 2021-12-13 14:25:05 -08:00
Nikolaj Bjorner fcdf8d4948 include atomic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-13 11:40:45 -08:00
Nikolaj Bjorner b85f2f7e86 #5704 2021-12-12 21:10:07 -08:00
Nikolaj Bjorner 0a7e003709 this one is for you Nuno 
- pull request might have new bugs given that build is broken.
- this test doesn't expose race conditions under simple tests, yet. It is a starting point.
- run under cuzz (app-verifier) should expose races, this is what it was made for.
 2021-12-12 17:51:05 -08:00
Nikolaj Bjorner 96e871c826 add stub for testing updates to scoped_timer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-12 12:31:23 -08:00
Calvin Loncaric 0405a597d4
Fix return type of as_int64 (#5703) 2021-12-09 14:39:38 -08:00
Nikolaj Bjorner 51fa40ece5 fix spelling 2021-12-09 10:23:37 -08:00
Nikolaj Bjorner b69ad786f2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-08 09:04:13 -08:00
Nikolaj Bjorner e45ae32685 unsound equality propagation #5676 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-08 09:02:05 -08:00
Nikolaj Bjorner a5bd115235 replace_re axiom placeholder 
@ahelwer - illustrates placeholder for one approach for axiomatizing replace_re
 2021-12-08 03:40:24 -08:00
Nikolaj Bjorner 773a2ae7bc na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 15:08:43 -08:00
Nikolaj Bjorner 60d5a004ce na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 14:25:07 -08:00
Nikolaj Bjorner 04906bd957 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 14:21:46 -08:00
Nikolaj Bjorner 36f510553a na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 14:20:47 -08:00
Nikolaj Bjorner d74ff29c25 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 13:55:31 -08:00
Nikolaj Bjorner 9f2b18cac5 add tactic name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-07 13:37:57 -08:00
Nikolaj Bjorner e3bd5badf2 pass through for unary tactical 2021-12-07 10:45:03 -08:00
Nikolaj Bjorner 1e95fb44d1 add ability to register expressions during callback 2021-12-07 09:47:05 -08:00
Nikolaj Bjorner 50d50cdb48 register forbidden functions with reduce_args for user-propagator 2021-12-07 09:03:19 -08:00
Nikolaj Bjorner 658a334ecf clear tactic user propagate state on solver destructor 2021-12-07 03:14:50 -08:00
Nikolaj Bjorner fdc253afdd
update arithmetic contract for unbounded (#5696) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-06 08:19:18 -08:00
Lev Nachmanson 9b4f3a7075
start using lar_solver::is_feasible() (#5697) 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-12-06 08:16:57 -08:00
Lev Nachmanson 7758b519bc
Handle correctly cancelled run (#5695) 
* remove the bound on total iterations in simplex

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove unncesseray checks in  get_freedom_interval_for_column()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix the build of test-z3

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Revert "remove unncesseray checks in  get_freedom_interval_for_column()"

This reverts commit 6770ed85e3.

* optimize get_freedom_interval_for_column() for feasible case

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add function lar_solver::status_feasible

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* rename status_is_feasible() to is_feasible()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix the linux build

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-12-05 18:38:37 -08:00
Nikolaj Bjorner f0e9363e78 fix bug in smt_tactic_core for translating user-ids 2021-12-05 11:13:27 -08:00
Nikolaj Bjorner 0d055b83eb update input for doxygen #5400 2021-12-05 09:04:18 -08:00
Nikolaj Bjorner c845b22c15 fix translation for equality propagation 2021-12-04 11:55:36 -08:00
Nikolaj Bjorner 1b0ac4940b prevent stale user-propagators from being used on the same tactic after it was applied. 2021-12-04 11:51:00 -08:00
Nikolaj Bjorner da765355e8 don't rely on cleanup 2021-12-04 11:48:41 -08:00
Nikolaj Bjorner 3d528c8ef6 typo 2021-12-04 11:19:49 -08:00
Nikolaj Bjorner eae567ac3d indirection for user ids 2021-12-04 11:04:32 -08:00
Nikolaj Bjorner 68b072e7f1 only use setup_and_check if there is no user propagator set. 2021-12-04 09:22:25 -08:00
Nikolaj Bjorner 1618c970df adding checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-03 13:17:48 -08:00
Nikolaj Bjorner 970347e797 infeas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-03 13:00:52 -08:00
Nikolaj Bjorner 0077ddf33c try delay init for user propagator in smt_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-03 09:45:07 -08:00
Nikolaj Bjorner 41aa7d7b60 stack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-02 09:00:51 -08:00
Nikolaj Bjorner bfd61fec00 enable user propagation on tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-02 08:28:52 -08:00
Nikolaj Bjorner 71cbb160d2 fix regression from today, see #5676 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-01 14:29:53 -08:00
Nikolaj Bjorner 87aec8819f fix #5687 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-01 10:08:29 -08:00
Nikolaj Bjorner c6a5aa0cc4 try th_lemma, update documentation of api functions for creating strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-01 09:21:02 -08:00
Nikolaj Bjorner 3b4f976118 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-30 19:15:03 -08:00
Nikolaj Bjorner 4daba290b1 change user propagation to apply scheme similar to theory_recfun 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-30 19:12:15 -08:00
Nikolaj Bjorner 3c1aedf219 fixing #5473 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-30 17:08:28 -08:00
Nikolaj Bjorner 9e51691285 add virtual destructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-29 20:02:12 -08:00
Nikolaj Bjorner b5efb87118 base -> core 2021-11-29 19:55:10 -08:00
Nikolaj Bjorner 959f4c9440 rename files to theory_user_propagator 2021-11-29 19:44:58 -08:00
Nikolaj Bjorner 5857236f2f introducing base namespace for user propagator 2021-11-29 19:41:30 -08:00
Nikolaj Bjorner c083aa82ee add debug information in user-propagate #5687 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-29 08:59:53 -08:00
Nikolaj Bjorner 1e9e52a58f #5641 2021-11-29 08:59:53 -08:00
Lev Nachmanson d50c4bfcc1 remove an unused var 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-11-28 09:44:50 -08:00
Nikolaj Bjorner d50bfc6a50 #5641 2021-11-25 18:01:35 +01:00
Nikolaj Bjorner 833dd62623 fix #5681 2021-11-24 13:24:31 +01:00
Nikolaj Bjorner e8f5a29c31 fix #5679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-22 19:37:10 +01:00
Nikolaj Bjorner fee4821106 include thread 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 21:06:07 +01:00
Nikolaj Bjorner a7d24788c3 wasm build issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 20:45:36 +01:00
Nikolaj Bjorner 741c5f43f4 Merge branch 'master' of https://github.com/z3prover/z3 2021-11-19 11:03:08 -08:00
Nikolaj Bjorner ca2c2bb802 ensure smt2log works with multi-threaded consumers, ease scenarios around #5655 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 11:02:50 -08:00
Nikolaj Bjorner 4928c28e63 fix #5675 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 08:42:32 -08:00
Nikolaj Bjorner 99d5215956 revert use of f format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 00:01:19 -08:00
Nikolaj Bjorner f83367a11e mac builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 22:39:30 -08:00
Nikolaj Bjorner 518ef9f916 fix #5674 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 21:14:50 -08:00
Nikolaj Bjorner c826b64e35 prepare release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-16 09:41:51 -08:00
Nikolaj Bjorner b6f7deacf4 fix #5663 2021-11-12 11:36:42 -08:00
Nikolaj Bjorner 3c16edc8d3 check for v1 == v2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-12 09:11:17 -08:00
Nikolaj Bjorner 63ac2ee0d1 #5614 turn on / off options to get better performance. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-11 17:54:46 -08:00
Nikolaj Bjorner b28a8013fe #5653 
fix performance bottleneck in static features
 2021-11-11 13:30:38 -08:00
Nikolaj Bjorner 3a9656bc59 fixing issues with user propagator from python 
"fresh" remains broken (not working yet).
 2021-11-07 17:04:11 -08:00
Nikolaj Bjorner f2fcbc7cb7 capture values not reference 2021-11-07 13:43:56 -08:00
Nikolaj Bjorner af2cc460a9 #5646 2021-11-03 08:53:48 -07:00
Nikolaj Bjorner dd1e0fc561 #5643 2021-11-03 08:53:48 -07:00
Clemens Eisenhofer 091079e58c
Added user propagator example (#5625) 
* Added user propagator example

* User propagator example code refactoring
(+ removed unused parameter warning)

* Moved user-propagator example to its own directory
 2021-11-02 15:03:02 -07:00
Nikolaj Bjorner 87d4ce2659 working on #5614 
there are some different sources for the performance regression illustrated by the example. The mitigations will be enabled separately:
- m_bv_to_propagate is too expensive
- lp_bound_propagator misses equalities in two different ways:
   - it resets row checks after backtracking even though they could still propagate
   - it misses equalities for fixed rows when the fixed constant value does not correspond to a fixed variable.

FYI @levnach
 2021-11-02 14:55:39 -07:00
Nikolaj Bjorner a94e2e62af build warnings 2021-11-02 14:55:38 -07:00
Henrich Lauko 96671cfc73
Add and fix a few general compiler warnings. (#5628) 
* rewriter: fix unused variable warnings

* cmake: make missing non-virtual dtors error

* treewide: add missing virtual destructors

* cmake: add a few more checks

* api: add missing virtual destructor to user_propagator_base

* examples: compile cpp example with compiler warnings

* model: fix unused variable warnings

* rewriter: fix logical-op-parentheses warnings

* sat: fix unused variable warnings

* smt: fix unused variable warnings
 2021-10-29 15:42:32 +02:00
Alexander Traud 1d45a33163
fix one typo and two misunderstandings for doxygen (#5633) 2021-10-29 15:35:05 +02:00
Alexander Traud d1592c6abf
fix misspelled \brief for doxygen (#5632) 2021-10-29 15:34:28 +02:00
Nikolaj Bjorner 4dad414161 fix performance regression after adding user declared functions to model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-28 05:49:15 +02:00
Alexander Traud f5f35f87d0
fix grouping for latest doxygen (#5626) 
Since doxygen 1.8.16, opening and closing a group must not be done as
C comment but as doxygen command. In other words, not one but two
asterisk characters are required so that doxygen finds a group.
 2021-10-27 23:46:31 +02:00
Nikolaj Bjorner 125eae06bd #4869 load datatype parsing for HORN logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-26 11:54:29 +02:00
Nikolaj Bjorner 61eb8d1908 add ref for regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-26 11:39:13 +02:00
Nikolaj Bjorner aa5b4b8c77 strengthen contract for log_axiom_instantiation #5621 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-26 09:49:44 +02:00
Nikolaj Bjorner bdecc25619 strengthen contract for log_axiom_instantiation #5621 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-26 09:49:44 +02:00
Margus Veanes efcad5ff35
fixed nullability bug in the if-then-else info (#5620) 2021-10-26 09:11:07 +02:00
Nikolaj Bjorner 075769c4c0 try get_string contents again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-25 16:03:40 +02:00
Nikolaj Bjorner 45681b4c6e update API type annotation to make it OCaml friendly 2021-10-25 13:43:15 +02:00
Nikolaj Bjorner 3036b88f09 support threading for TRACE mode 2021-10-25 13:35:32 +02:00
Nikolaj Bjorner 3a3cef8fce #5615 - update documentation and use non-encoded versions for ASCII characters in get_lstring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-23 18:21:51 +02:00
Nikolaj Bjorner 7f41d6140f use some suggestions from #5615 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-22 12:39:55 -04:00
Nikolaj Bjorner 051616385f remove deprecated escape string from Julia bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-21 19:14:12 -04:00
Nikolaj Bjorner f05ac8a429 updated C++ API for escaped and unescaped strings #5615 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-21 14:52:59 -04:00
Nikolaj Bjorner 05e7ed9637 add API to access unescaped strings, update documentation of Z3_get_lstring, #5615 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-21 11:30:03 -04:00
Nikolaj Bjorner 6eed885379 print bounded terms for better efficiency 2021-10-21 10:42:39 -04:00
Nikolaj Bjorner 13da6a02a6 add handling of quantifiers #5612 2021-10-20 12:27:56 -04:00
Nikolaj Bjorner 839a0852fe Merge branch 'master' of https://github.com/z3prover/z3 2021-10-19 12:24:41 -04:00
Nikolaj Bjorner 86147d01ea #5605 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-19 12:24:29 -04:00
Nikolaj Bjorner f9dde2e8a4 #5605 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-19 12:21:54 -04:00
CEisenhofer 3557e0b0c5
Added eq/fixed/final functions in C++ user propagator as methods (#5607) 2021-10-19 10:48:31 -04:00
Nikolaj Bjorner fc3a701888 push-pop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-18 15:36:48 -07:00
Nikolaj Bjorner d5e5dcfe45 add nff and auto-relevant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-18 15:32:55 -07:00
Nikolaj Bjorner bc2020a39b #5604 
retain array interpretation when available
 2021-10-17 20:24:26 -07:00
Nikolaj Bjorner 115203e87c fixes to sat.euf ematching #5573 2021-10-16 15:52:37 -07:00
Margus Veanes f78546cd7c
fixed bug of computing butlast of a sequence (#5602) 2021-10-15 18:02:51 -07:00
Nikolaj Bjorner fb9fa1b7d2 updated printer 2021-10-15 17:56:54 -07:00
Margus Veanes cb120c93f4
Regex range bug fix (#5601) 
* added a missing derivative case for nonground range

* further missing cases and a bug fix in re.to_str
 2021-10-15 15:30:55 -07:00
Simon Cruanes 6302b864c8
tweak GC in OCaml bindings (#5600) 
* feat(api/ml): use custom block hints to guide the GC

this forces the GC to collect garbage when a few _large_ objects
(solver, etc.) are dead. The current code would let arbitrarily many
such objects die and not trigger a GC (which would have to come from
OCaml code instead)

* tuning

* try to use caml_alloc_custom_mem with fake sizes

* try to fix leak by explicitly finalizing OCaml context

* chore: use more recent ubuntu for azure CI

* remove finalizer causing segfault in example
 2021-10-14 12:46:14 -07:00
Nikolaj Bjorner f60ed2ce92 #5591 2021-10-13 21:38:36 -07:00
Nikolaj Bjorner 7b341313d5 #5593 2021-10-13 17:50:56 -07:00
Nikolaj Bjorner fd77f0c111 fix #5594 2021-10-13 17:17:05 -07:00
Nikolaj Bjorner 96e117d78c Update smt_context.cpp 2021-10-12 17:10:12 -07:00
Nikolaj Bjorner c15968aa9e fix #4901 2021-10-12 17:10:04 -07:00
Nikolaj Bjorner 9a76bf0aa2 #5591 
nth issue
 2021-10-12 13:59:28 -07:00
Christoph M. Wintersteiger 58fd4fc860
Merge pull request #5550 from wintersteiger/cwinter_fpa_fixes 
Assorted fixes for floats
 2021-10-12 18:24:49 +01:00
Nikolaj Bjorner 52032b9ef8 #5467 2021-10-12 10:16:15 -07:00
Christoph M. Wintersteiger b471ebdf1c
Revert "Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it." 
This reverts commit f80fdb4ea3a762cfe95daa0321d9875cfa00c7ae.
 2021-10-12 12:45:11 +00:00
Christoph M. Wintersteiger 738783a26c
Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it. 2021-10-12 12:45:11 +00:00
Christoph M. Wintersteiger c24f438e51
Fix for mk_to_fp_float; pertains to #4841 2021-10-12 12:45:10 +00:00
Christoph M. Wintersteiger 00e8ea7962
Make terms that are internalized on the fly relevant 2021-10-12 12:45:10 +00:00
Christoph M. Wintersteiger 8e69f76784
Add additional equality in theory_fpa 2021-10-12 12:45:09 +00:00
Christoph M. Wintersteiger f1acc4b78a
Make fpa2bv debug symbol names optional 2021-10-12 12:45:09 +00:00
Christoph M. Wintersteiger 515a2a771e
Whitespace 2021-10-12 12:45:09 +00:00
Christoph M. Wintersteiger e8d6d97ba3
Refine fpa_decl_plugin::is_unique_value 2021-10-12 12:45:08 +00:00
Christoph M. Wintersteiger 12c32663c6
Fix error messsages 2021-10-12 12:45:08 +00:00
Nikolaj Bjorner c3549ec784 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-11 11:03:45 -07:00
Nikolaj Bjorner 73102cffcb fix #5589 2021-10-11 11:03:45 -07:00
Nikolaj Bjorner 75702c3631 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-11 11:03:45 -07:00
Nikolaj Bjorner 0fc9f1d46a fix max/min length to handle concatenation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-09 16:20:32 -07:00
Andrew V. Jones f1b8376739
Rename 'user' to 'user_solver' #5586 (#5587) 
Issue #5586 reported that Android builds (targetting, e.g., x86) failed
to compile due to a conflict between:

* `struct user` in `sys/user.h`; and
* `namespace user` in z3's `user_solver.h`

This issue is resolved by renaming `namespace user` to `namespace
user_solver` (matching the header name) to avoid this conflict.

Reported-by: Jamie Collinson <jamiecollinson@gmail.com>

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
 2021-10-09 15:07:37 -07:00
Nikolaj Bjorner bfa960c2ce fix internalize regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-08 14:48:17 -07:00
Margus Veanes 146f4621c5
Updated regex derivative engine (#5567) 
* updated derivative engine

* some edit

* further improvements in derivative code

* more deriv code edits and re::to_str update

* optimized mk_deriv_accept

* fixed PR comments

* small syntax fix

* updated some simplifications

* bugfix:forgot to_re before reverse

* fixed PR comments

* more PR comment fixes

* more PR comment fixes

* forgot to delete

* deleting unused definition

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-08 13:04:49 -07:00
Nikolaj Bjorner c0c3e685e7 disable all propagation until ematch incompleteness is fixed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-05 11:25:35 -07:00
Nikolaj Bjorner 94cc4ead72 remove arith_lhs simplification from preamble tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-05 10:55:38 -07:00
Nikolaj Bjorner 33f4e65fa9 redo bindings/fingerprints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-05 10:15:56 -07:00
Nikolaj Bjorner 281fb67d88 unit propagate with fingerprints 2021-10-04 20:01:46 -07:00
Nikolaj Bjorner 8a85cfdb12 fix #5579 - 
It is only possible to reach this case when new assertions are created.
 2021-09-30 09:32:34 -07:00
Nikolaj Bjorner cbe7dd4a48 missing continue fixes unsound sat result from #5573 2021-09-29 14:26:09 -07:00
Nikolaj Bjorner ff723f15ff Update z3++.h 2021-09-29 12:19:02 -07:00
Nikolaj Bjorner 62fd22f555 disable macro finder tactic if there are recursive functions fix #5574 2021-09-29 09:33:52 -07:00
Nikolaj Bjorner 137e5c5263 fix tmp_eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 14:28:41 -07:00
Nikolaj Bjorner 67ae75bac7 fix tmp_eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 14:27:46 -07:00
Nikolaj Bjorner da124e4275 tune q-eval and q-ematch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 13:41:37 -07:00
Nikolaj Bjorner 92c1b600c3 tuning eval 2021-09-28 09:56:00 -07:00
Nikolaj Bjorner 2e176a0e02 count lazy bindings 2021-09-28 08:27:46 -07:00
Nikolaj Bjorner 3abecc3428 add extra commands to API parser 2021-09-27 14:19:43 -07:00
Nikolaj Bjorner 6c71baf77b lifting iff to binary 2021-09-27 03:45:54 -07:00
Nikolaj Bjorner d174f87c5e #5532 2021-09-21 20:21:23 -07:00
Nikolaj Bjorner 18d1b368d1 #5532 2021-09-21 20:12:32 -07:00
Nikolaj Bjorner cabd5b10fa #5532 2021-09-21 18:56:55 -07:00
Nikolaj Bjorner de20bffafe import goodies from ps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 11:13:03 -07:00
Nikolaj Bjorner 708602dfbb fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 08:56:13 -07:00
Nikolaj Bjorner 2e96557827 fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 08:55:28 -07:00