Will it matter anything if "The logic QF_BV is not reducible to any SMTLib2 standard logic"

11 views
Skip to first unread message

陳宏毅

unread,
Sep 11, 2017, 11:16:55 AM9/11/17
to pySMT
Dear all:

I have tried to output my constraint formula into a smt2 file.
Based on:

from pysmt.smtlib.script import *
s = smtlibscript_from_formula(f)
print(s) # or s.serialize(file_handle) to directly dump the smt2 code to file
s.to_file( "String_of_FileName"  , daggify=True) # or s.serialize(file_handle) to directly dump the smt2 code to file

Then the warning message shows that:

"sys:1: UserWarning: The logic QF_BV is not reducible to any SMTLib2 standard logic. Proceeding with non-standard logic 'QF_BV'"

Will it matters anything, or it's Okey to ignore it?

P.S: the whole formula is constructed by Bit-Vector calculations.

Marco Gario

unread,
Sep 11, 2017, 1:35:43 PM9/11/17
to 陳宏毅, pySMT
Hi, the message might be a bug. 

In any case, the idea of the message is that you might be using a logic that does not have a name in smtlib. This is not your case, and as long as the solver is solving it, you are fine. 

--
You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+unsubscribe@googlegroups.com.
To post to this group, send email to py...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/39e8fb71-4b7d-4eb2-b00f-7e6328b7fd44%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Marco Gario

unread,
Sep 16, 2017, 6:39:37 AM9/16/17
to pySMT
I cannot reproduce. If you could share the formula (in smt format or the code to generate it) that would be great!
Reply all
Reply to author
Forward
0 new messages