mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity
16461 commits 23 branches 48 tags 157 MiB
Commit graph

13897 commits

Author SHA1 Message Date
Nikolaj Bjorner 3828130791 fix #5922 use 0u to help type inference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-24 14:05:14 -10:00
Nikolaj Bjorner 32233e1bf1 set default to true to avoid regression failures 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-23 12:20:53 -07:00
Nikolaj Bjorner 365b8f3281 change default to _not_ include auxiliary functions in model as this seems to break fewer' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-23 09:51:06 -07:00
Nikolaj Bjorner d790523c59 #5917 
Add model.user_functions (default true) to control whether user functions are added to the model.
 2022-03-23 09:49:44 -07: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 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 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 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
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 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 669a1d63da na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-18 16:36:16 -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 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 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
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
Nikolaj Bjorner e839e18381 minimal addition to rewrite bit-vector to character conversion using constant folding. 2022-03-10 17:31:17 -08:00
Nikolaj Bjorner 8f2ea90db1 Merge branch 'master' of https://github.com/Z3Prover/z3 2022-03-10 17:09:36 -08:00
Nikolaj Bjorner 081c62d006 allow range comparison for bit-vectors and int/real 2022-03-10 17:08:49 -08:00
Nikolaj Bjorner 580012e19f fix #5894 
expp is not implemented. This is the second time a fuzz bug reports it. Instead of closing the bug, just disable code path as fuzzers are not considering the comment from previous bug.
 2022-03-10 09:45:09 -08:00
Hari Govind V K f26c12a9ad
fix #5882. Use model true when inlining (#5892) 2022-03-09 12:31:39 -08:00
Nuno Lopes 43f7636826 remove some copies/moves 2022-03-09 12:46:41 +00:00
Nikolaj Bjorner 1d224d1bcd na 2022-03-08 08:51:00 -08:00
Nikolaj Bjorner c6f8ee33d4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-08 08:36:19 -08:00
Nikolaj Bjorner 3293aeb7c7 na 2022-03-08 08:36:19 -08:00
John Fleisher 97c7ce63b5
Clean up build warnings (#5884) 
* Clean up warnings in compile for documentation notes

* remove snk from local build

Co-authored-by: jfleisher <jofleish@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-07 12:55:30 -08:00
Lorenzo Veronese e3568d5b47
Handle additional cases in rule_properties::check_accessor (#5821) 
* Handle additional cases in rule_properties::check_accessor

* Walk parents depth first in rule_properties::check_accessor
 2022-03-07 07:49:59 -08:00
Nikolaj Bjorner 882fc31aea doc strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 15:25:05 -08:00
Nikolaj Bjorner b0c0f4d1f4 fix #5876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 15:07:45 -08:00
Nikolaj Bjorner 3e51b69a9a no fun! 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 15:03:02 -08:00
Nikolaj Bjorner 87e6f103c6 commenting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 14:00:07 -08:00
Nikolaj Bjorner 676ba78600 fix else case: it is first argument of const array 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 13:10:02 -08:00
John Fleisher 35d26bc282
NativeModel: TryGetArrayValue (#5881) 
* WiP:  Disposable, MkAdd, MkApp, MkBool, MkBoolSort, MkBound, MkBvSort, MkFalse, MkTrue, MkIntSort

* WiP: Native z3 mk_ functions

* WiP: mk_ functions for NativeContext

* WiP: add utility functions for getting values

* WiP: Adding more native utility functions

* native model pull

* WiP: NativeContext additions for array access

* WiP: use Z3_symbol in place of managed Symbol

* WiP: add solver, model, and array methods

* WiP: MkSimpleSolver, MkReal

* WiP: GetDomain GetRange

* WiP: MkExists

* Override for MkFuncDecl

* MkConstArray, MkSelect

* WiP: code cleanup

* migrate Context reference to NativeContext

* remove local signing from PR

* minor code cleanup

* Sorts to properties, fix usings,

* make IntSort property

* sort using

* IntSort, RealSort - properties

* WiP: get array value update

Co-authored-by: jfleisher <jofleish@microsoft.com>
 2022-03-03 13:06:30 -08:00
Nikolaj Bjorner 248a3676af na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 11:40:29 -08:00
Nikolaj Bjorner e1e8d15827 stub out array serialization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 11:38:23 -08:00
Nikolaj Bjorner cd324a4734 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 11:07:00 -08:00
Nikolaj Bjorner 8d1276fa60 using directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 11:03:31 -08:00
John Fleisher a08be497f7
NativeContext, NativeSolver, NativeModel - updates for Pex (#5878) 
* WiP:  Disposable, MkAdd, MkApp, MkBool, MkBoolSort, MkBound, MkBvSort, MkFalse, MkTrue, MkIntSort

* WiP: Native z3 mk_ functions

* WiP: mk_ functions for NativeContext

* WiP: add utility functions for getting values

* WiP: Adding more native utility functions

* native model pull

* WiP: NativeContext additions for array access

* WiP: use Z3_symbol in place of managed Symbol

* WiP: add solver, model, and array methods

* WiP: MkSimpleSolver, MkReal

* WiP: GetDomain GetRange

* WiP: MkExists

* Override for MkFuncDecl

* MkConstArray, MkSelect

* WiP: code cleanup

* migrate Context reference to NativeContext

* remove local signing from PR

* minor code cleanup

Co-authored-by: jfleisher <jofleish@microsoft.com>
 2022-03-03 10:41:12 -08:00
Nikolaj Bjorner 811cd9d48d add example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-03 09:14:47 -08:00
Nikolaj Bjorner ee18c5070c add stubs for injective function axioms, add some parameter functions 2022-03-03 09:09:03 -08:00
Nikolaj Bjorner 757cf7622d sketch ArrayValue, add statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-02 10:59:19 -08:00
Nikolaj Bjorner 80506dfdfa sketch ArrayValue, add statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-02 10:55:39 -08:00
Nikolaj Bjorner bf14aeb1bd stub out nativesolver 2022-03-02 10:06:38 -08:00
Nikolaj Bjorner bbadd17d56 fix #5874 2022-03-02 08:46:28 -08:00
Nikolaj Bjorner 5f79a977fb use conventions from Context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-01 14:27:57 -08:00
Nikolaj Bjorner c812d1e890 update native func interp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-01 14:07:20 -08:00
Nikolaj Bjorner 61d2654770 quantifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-01 13:18:18 -08:00
Nikolaj Bjorner deeb5e9921 finish NativeModel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-01 12:40:03 -08:00
Nikolaj Bjorner c0826d58bf add stubs for native model and func interp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-01 12:11:10 -08:00
Nikolaj Bjorner deaad86d6a nit 2022-03-01 12:11:10 -08:00
Nikolaj Bjorner 2b6dadcbc6 fix #5869 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-28 17:02:13 -08:00
Nikolaj Bjorner 302c0d178c fix #5867 2022-02-26 09:52:23 -08:00
Clemens Eisenhofer 412b05076c
User-functions fix (#5868) 2022-02-26 09:21:01 -08:00
Nuno Lopes 689e2d41de remove a bunch of unneeded memory allocations 2022-02-25 16:08:23 +00:00
Nikolaj Bjorner 7f149a36d7 refining model update rules for del_rule #5865 #5866 2022-02-25 08:03:46 -08:00
Nikolaj Bjorner 30a2f2fd9d initial stab at NativeContext 2022-02-25 07:56:36 -08:00
Nikolaj Bjorner f2e712b0d6 throttle is_compatible to check variables at most once 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-23 08:45:22 -08:00
Nikolaj Bjorner 7b4f1ed530 missing initialization of m_user_propagator, disable unsound in-processing in pb_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-23 04:49:42 -08:00
Nikolaj Bjorner 6be0a66b38 fix #5863 2022-02-22 13:00:20 -08:00
Nikolaj Bjorner 6af170b058 fix #5861 
sigh
 2022-02-22 11:26:09 -08:00
Nikolaj Bjorner c2f1bdc099 fix #5862 2022-02-22 08:05:05 -08:00
Nikolaj Bjorner 11030fc81d disable unsound mk_seq_butlast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-21 18:56:49 -08:00
Nikolaj Bjorner ea0876b6d6 add lambda definitions during ast translation #5820 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-21 18:05:29 -08:00
Nikolaj Bjorner d06c51d517 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-21 17:46:54 -08:00
Nikolaj Bjorner 061e94d723 #5858 
COI model converter has to use constraints from the body and work in disjunctive mode. It needs a pre-condition that the body does not depend on other rules, in the case that it is used in a different pre-processing step for in-lining. The in-lined occurrence of the predicate has to correspond to the model construction version.
 2022-02-21 17:45:00 -08:00
Nikolaj Bjorner e8d4804dbb
Revert "use horn_subsume_model_converter in coi filter (#5844)" (#5859) 
This reverts commit 09da87dc85.
 2022-02-21 04:33:52 -08:00
Nikolaj Bjorner b843618051 fix #5798 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-20 13:54:15 -08:00
Nikolaj Bjorner 5c2624950b #5849 2022-02-20 09:52:42 -08:00
Nikolaj Bjorner 1e463955c2 #4889 avoid double internalize of bvle 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-20 09:09:28 -08:00
Nikolaj Bjorner f66b4f0880 fir #5856 2022-02-20 15:32:41 +02:00
Nikolaj Bjorner d0d4ab7955 #5820 2022-02-20 10:33:29 +02:00
Nikolaj Bjorner ff5d210e81 na 2022-02-20 10:33:15 +02:00
Nikolaj Bjorner 4d184fe65d skip expensive equality rewriting of Booleans 2022-02-20 10:31:10 +02:00
Nikolaj Bjorner 10b611b3ba fix #5850 2022-02-20 10:30:52 +02:00
Nikolaj Bjorner 91045d3e4a two words 2022-02-20 10:29:57 +02:00
Nikolaj Bjorner 9a1a72867c Add str.<= and str.< to Java API 2022-02-20 10:29:38 +02:00
Nikolaj Bjorner 7091b1c856 add additional regex operators to API 2022-02-20 10:29:18 +02:00
Nikolaj Bjorner 2e00f2f32d
Propagator (#5845) 
* user propagator without ids

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

* user propagator without ids

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

* fix signature

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

* references #5818

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

* fix c++ build

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

* switch to vs 2022

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

* switch 2022

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

* Update propagator example (I) (#5835)

* fix #5829

* na

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

* switch to vs 2022

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

* Adapted the example to the changes in the propagator

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* context goes out of scope in stack allocation, so can't used scoped context when passing objects around

* parameter check

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

* add rewriter

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

* Fixed bug in user-propagator "created" (#5843)

Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
 2022-02-17 09:21:41 +02:00
mbergen 2e15e2aa4d
Add access to builtin special relations (Context::mkLinearOrder and Context::mkPartialOrder ) to Java API (#5832) 
* Add mkLinearOrder

* reorder arguments to match definition, add short comment

* add partial order

* add comments
 2022-02-16 23:37:20 +02:00
Qix 9cf50766a6
fix compiler warnings under clang (#5839) 2022-02-16 23:36:34 +02:00
Valentine Sobol 09da87dc85
use horn_subsume_model_converter in coi filter (#5844) 2022-02-16 23:35:58 +02:00
Nikolaj Bjorner 5bbb8fb807 add bail #5825 2022-02-16 23:30:12 +02:00
Nikolaj Bjorner 33985ebcf5 update expected 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 19:14:54 +02:00
Nikolaj Bjorner 6202cd5394 fix #5842 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 17:38:19 +02:00
Nikolaj Bjorner aa6ec418e3 move idiv test to after cuts/branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-14 19:50:49 +02:00
Nikolaj Bjorner 9a4d6cee6c overhead with push-ite on shared terms 2022-02-14 19:36:14 +02:00
Nikolaj Bjorner 3d26b501e7 fix #5827 #5828 2022-02-14 10:31:04 +02:00
Nikolaj Bjorner 81e94b2154 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-09 12:10:01 +02:00
Nikolaj Bjorner 07d02ea415 fix #5829 2022-02-09 12:08:36 +02:00
Nikolaj Bjorner 0059e88036 fix #5808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-07 20:10:32 +02:00
Nikolaj Bjorner 9958cab5cc fix #5808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-07 07:43:30 +02:00
Nikolaj Bjorner 3f3d058567 extract also units from search state 2022-02-07 06:16:22 +02:00
Nikolaj Bjorner 03ff3201b9 block recursive definitions with lambdas until they are properly supported #5813 2022-02-06 08:57:58 +02:00
Nikolaj Bjorner 1c10ce4070 #5815 - surface multi-arity arrays over python API 2022-02-06 08:40:56 +02:00
Nikolaj Bjorner 8a84cacfea add tuple support for __getitem__ #5815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-06 04:02:12 +02:00
Nikolaj Bjorner e9dad84b85 update documentation comments 2022-02-06 03:35:32 +02:00
Nikolaj Bjorner 9d655cc658 track all unhandled operators instead of latest 2022-02-04 22:07:29 -08:00
Nikolaj Bjorner 474949542e Merge branch 'master' of https://github.com/z3prover/z3 2022-02-04 13:08:59 -08:00
Nikolaj Bjorner 05e28e4344 fix #5812 2022-02-04 13:08:52 -08:00
Nikolaj Bjorner 6a412f7f04 allow to pass Booleans as arguments to arithmetic expressions 2022-01-31 12:00:54 -08:00
Nikolaj Bjorner 994c7ef52d format 2022-01-31 12:00:26 -08:00
Nikolaj Bjorner 1e0d49512b call mux finder 2022-01-31 12:00:16 -08:00
Nikolaj Bjorner 4392b88718 return negated literal when expression is "not" 2022-01-31 12:00:00 -08:00
Nikolaj Bjorner 7ddfc54250 shortcut negation 2022-01-31 11:58:02 -08:00
Nikolaj Bjorner f3fc6a50f3 formatting 2022-01-31 11:57:42 -08:00
Nikolaj Bjorner 6422b783b2 fix mux extraction to check for top-level assertion 2022-01-31 11:57:16 -08:00
Nikolaj Bjorner 62bb234251 expose extract roots as separate 2022-01-31 11:56:44 -08:00
Nikolaj Bjorner a326ad4cd9 flag incomplete on lambdas #5803 2022-01-31 11:54:06 -08:00
Nikolaj Bjorner a189ca8b60 truncation directive #5805 2022-01-31 10:50:46 -08:00
Nikolaj Bjorner 773e829c58 #5804 2022-01-31 10:16:09 -08:00
Nikolaj Bjorner 913b90f7aa fix #5802 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-30 10:42:34 -08:00
Nikolaj Bjorner 2551631957 mul overflow #5797 2022-01-29 09:15:38 -08:00
Nikolaj Bjorner 5e81c1220c #5797 probably still wrong wrt underflow. 2022-01-27 12:48:15 -08:00
Nikolaj Bjorner 9e5b6e0c9c #5778 2022-01-27 12:12:58 -08:00
Nikolaj Bjorner 4da930b490 #5794 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 10:50:48 -08:00
Nikolaj Bjorner a621041308 fix #5795 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 10:45:38 -08:00
Nikolaj Bjorner 461e71017d fix #5792 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 15:54:44 -08:00
Nikolaj Bjorner c6539deb61 fixing null check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 17:25:42 +01:00
Nikolaj Bjorner 435f79eab0 tup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 16:40:55 +01:00
Nikolaj Bjorner 9294b2ceb2 created 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 16:33:23 +01:00
Nikolaj Bjorner 3de9d37772 fix overrides for created_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 16:24:08 +01:00
Nikolaj Bjorner bf6454dccc throw error if created-eh has not been registered 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 13:01:57 +01:00
Nikolaj Bjorner ea6827505e add missing callback to m_created_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 10:13:09 +01:00
Nikolaj Bjorner f639a7e1bc add marker for top-level expression in rule. 2022-01-24 15:20:44 +01:00
Nikolaj Bjorner 61ab72b6a3 fix #4869 2022-01-24 15:14:47 +01:00
Nikolaj Bjorner 3b8c0b7ae6 fix #5791 2022-01-24 15:11:24 +01:00
Nikolaj Bjorner 20f9814939 fix #5789 
fix incorrect constant folding
 2022-01-24 09:42:14 +01:00
Nikolaj Bjorner d02235fe08 #5778 
not really specific to euf.true, but about rem(x,0) semantics that should align with mod semantics. It also reproduces without sat.euf=true.
 2022-01-22 16:16:48 +01:00
Hennadii Chernyshchyk 85f6456655
Add missing constness (#5787) 2022-01-21 15:32:25 +01:00
Nikolaj Bjorner 9969809745 #5778 2022-01-21 09:40:06 +01:00
Nikolaj Bjorner a1f7676c81 remove assertion - literals could be assigned but propagation incomplete 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-21 03:10:41 +01:00
Nikolaj Bjorner 007af9cb8a fix #5784 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-21 03:08:03 +01:00
Nikolaj Bjorner 17280846f8 added comments to explain #5781 2022-01-21 01:40:31 +01:00