Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Propagator #5845

Merged
merged 12 commits into from
Feb 17, 2022
Merged

Propagator #5845

merged 12 commits into from
Feb 17, 2022

Conversation

NikolajBjorner
Copy link
Contributor

No description provided.

NikolajBjorner and others added 12 commits February 9, 2022 04:38
@NikolajBjorner
user propagator without ids
16cbe45 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
user propagator without ids
59726d1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
fix signature
cad90aa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
references #5818
6200fef 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
fix c++ build
1530cbe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
switch to vs 2022
ddf1a6d 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
switch 2022
b773374 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@CEisenhofer @NikolajBjorner
Update propagator example (I) (#5835)
7f5b615 
* 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>
@NikolajBjorner
context goes out of scope in stack allocation, so can't used scoped c…
dfa28fa 
…ontext when passing objects around
@NikolajBjorner
parameter check
41005f6 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
add rewriter
aa85e48 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@CEisenhofer
Fixed bug in user-propagator "created" (#5843)
de0d9ce
@NikolajBjorner NikolajBjorner merged commit 2e00f2f into master Feb 17, 2022
@delixus-valliammal1
Copy link

[> _ No description provided. _

](#4977)
I have this problem. It is Mythril Library uses z3 and in that it is occurring while threads are at parallel processing.
the line 414 and 432 are error in ast.cpp. Can it be resolved. Or can it be avoided by some means by avoiding program to exit.?

@NikolajBjorner
Copy link
Contributor Author

you need to use a separate context per thread. Two threads cannot operate on expressions/solvers from the same context.

@delixus-valliammal1
Copy link

Now this flow instead of 414 and 432 in ast.cpp, giving error in rewrite_def.h in the line 224 and give error as "Unexpected Error"
Can you let us know what else to be changed?. Multiprocessing of threads and parallel is enabled now

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@NikolajBjorner @delixus-valliammal1 @CEisenhofer