Get UNSAT Core using Z3 from .smt2 file -

-


i need unsat core z3. contents of .smt2 file are:
(set-option :produce-unsat-cores true) (set-logic qf_aufbv ) (declare-fun () (array (_ bitvec 32) (_ bitvec 8) ) ) ; constraints (! (assert (bvslt (concat (select (_ bv3 32) ) (concat (select (_ bv2 32) ) (concat (select (_ bv1 32) ) (select (_ bv0 32) ) ) ) ) (_ bv10 32) ) ) :named ?u0) (! (assert (bvslt (_ bv10 32) (concat (select (_ bv3 32) ) (concat (select (_ bv2 32) ) (concat (select (_ bv1 32) ) (select (_ bv0 32) ) ) ) ) ) ) :named ?u1) (check-sat) (get-unsat-core) (exit)

i getting following output when running z3:
unsupported ; ! unsupported ; ! sat (error "line 11 column 15: unsat core not available")
new z3, can't understand happening here (i sure expression unsat).
thanks.

you use ! incorrectly. exclamation point used naming formulae (not asserts). see section 3.9.8 tutorial.

this should fix it: (assert (! (bvslt ...) :named ?u0)).


Comments

Post a Comment

Popular posts from this blog

python - TypeError: start must be a integer -

-
i trying draw 5 turtles, getting typeerror on line 25. here code: import turtle wn = turtle.screen() redrose = turtle.turtle() color = input("what background color be?") fillcolor_f = input("what color of rose be?") redrose.hideturtle() redrose.speed(30) redrose.penup() redrose.left(180) redrose.forward(175) redrose.right(90) redrose.forward(30) redrose.right(90) redrose.pendown() def drawrose(red): redrose.color("pink") redrose.fillcolor(fillcolor_f) redrose.fill(true) in range(red): redrose.forward(i) redrose.right(49) in range(5): drawrose(redrose) redrose.penup() redrose.forward(350) redrose.right(144) redrose.pendown() redrose.fill(false) drawrose(50) wn.bgcolor(color) i trying draw 5 roses, produces errors. doing in interactivepython.org. you recursively calling drawrose wrong parameter. on line 23 ( for in range(red): ) expect red integer...
Read more

c# - DevExpress RepositoryItemComboBox BackColor property ignored -

-
i have following code almost works properly; private void cbstatus_drawitem(object sender, listboxdrawitemeventargs e) { string item = e.item string; if (item != null) { switch (item) { case "1": e.appearance.forecolor = color.green; e.appearance.backcolor = color.green; break; case "2": e.appearance.forecolor = color.orange; e.appearance.backcolor = color.orange; break; case "3": e.appearance.forecolor = color.red; e.appearance.backcolor = color.red; break; } } } when dropdown shown, items forecolor correct, backcolor remains whatever backcolor of theme is; i.e. if i've got set dark theme, backcolor dark, cells in gridview, rather being green/orange/red. i've tried setting e.appearance.options.usebackcolor trying set e....
Read more

django - Creating multiple model instances in DRF3 -

-
1) create multiple model instances 1 api call, asked here: how create multiple model instances django rest framework? tried solution named in link, no success. i trying upload multiple files in 1 api call. result: files uploaded (only once overwrote perform_create) 1 instance created (if send 2 files, latter created instance). my code: class fileuploadserializer(serializers.modelserializer): def __init__(self, *args, **kwargs): many = kwargs.pop('many', true) super(fileuploadserializer, self).__init__(many=many, *args, **kwargs) class meta: model = fileupload read_only_fields = ('created', 'datafile', 'owner') class fileuploadviewset(viewsets.modelviewset): queryset = fileupload.objects.all() serializer_class = fileuploadserializer parser_classes = (multipartparser, formparser, ) def perform_create(self, serializer): file_list = self.request.data.getlist('file') ...
Read more