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

[陳宏毅]

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]

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]

I cannot reproduce. If you could share the formula (in smt format or the code to generate it) that would be great!