Crash on boolector_parse(_smt2) and 2 questions regarding parsing

[Skarrabor]

Hi,

i am having some issues with the parse functions.

If i try to parse a string my code crashes, yet in version 3.0.0 it worked fine.

I added the status flag and i am using version 3.2.0 newest git commit (448b3c6) on Ubuntu 18.04.

The code i use is below. (It crashes with boolector_parse as well, i used a dump from boolector as string input)

Also two questions regarding parsing:

Is it possible to manipulate the parsed formula, for example with push/pop?
Is it possible to add other formulas to the assertion stack after parsing?

Thanks for you help,

Daniel

My Code:

int32_t  result = 0;
int32_t status = 0;
char *errormsg;
 
char *arg2 = (char *) 0 ;
if (jarg2) {
  arg2 = (char *)(*jenv)->GetStringUTFChars(jenv, jarg2, 0);
  if (!arg2) return 0;
}


FILE *fptr = 0;

fptr = fopen("btortemp", "w+");
if(fptr==NULL) {
  perror("ERROR_INPUTFILE");
}
fputs(arg2, fptr);
fclose (fptr);
 
FILE *fout = 0;
fout = fopen("btortempout", "w+");
if(fout==NULL) {
  perror("ERROR_OUTPUTFILE");
}
fclose (fout);
 
result = boolector_parse_smt2(btor, fptr, "btortemp", fout, &errormsg, &status);

[Aina Niemetz]

Hi Daniel,

can you provide us with the input that triggers that problem?

As for your other questions, this should work -- if not, let us know.

Cheers,
Aina

On 2/16/20 6:56 PM, 'Skarrabor' via Boolector wrote:
> Hi,
> i am having some issues with the parse functions.
> If i try to parse a string my code crashes, yet in version 3.0.0 it
> worked fine.
> I added the status flag and i am using version 3.2.0 newest git commit
> (448b3c6) on Ubuntu 18.04.
> The code i use is below. (It crashes with boolector_parse as well, i
> used a dump from boolector as string input)
>
> Also two questions regarding parsing:
> Is it possible to manipulate the parsed formula, for example with push/pop?
> Is it possible to add other formulas to the assertion stack after parsing?
>
> Thanks for you help,
> Daniel
>
>
> My Code:
> |
>
>
> int32_t  result =0;
> int32_t status =0;
> char*errormsg;
>  
> char*arg2 =(char*)0;
> if(jarg2){
>   arg2 =(char*)(*jenv)->GetStringUTFChars(jenv,jarg2,0);
>   if(!arg2)return0;
> }
>
>
> FILE *fptr =0;
>

> fptr =fopen("btortemp","w+");

> if(fptr==NULL){
>   perror("ERROR_INPUTFILE");
> }
> fputs(arg2,fptr);
> fclose (fptr);
>  
> FILE *fout =0;

> fout =fopen("btortempout","w+");

> if(fout==NULL){
>   perror("ERROR_OUTPUTFILE");
> }
> fclose (fout);
>  
> result =boolector_parse_smt2(btor,fptr,"btortemp",fout,&errormsg,&status);
>
> |
>
>

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/boolector/eb1223d1-b290-45af-9671-5fc31e464e9d%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/eb1223d1-b290-45af-9671-5fc31e464e9d%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Skarrabor]

Hi Aina,

sorry for coming back so late.

I fixed the crash. The problem was on my side, sorry about that.

I do however have another question:

If i parse a String like:

"(set-logic QF_BV)
 (declare-fun x () (_ BitVec 8))
 (declare-fun y () (_ BitVec 8))
 (assert (= #b01100100  (bvmul x y)))"

without check-sat and call dump afterwards it dumps:

(set-logic QF_BV)
(assert true)
(check-sat)
(exit)

Is that wanted?

Basicly the behavior i would expect (want) is something like the ability to parse, push/pop maybe, parse more but using past parses, push/pop... repeat and call SAT later (for multiple formulas).

Kind regards,

Daniel

[Aina Niemetz]

Hi Daniel,

sorry for being late, too.

I get a very different dump with your input (current master):

(set-logic QF_BV)
(declare-fun x () (_ BitVec 8))
(declare-fun y () (_ BitVec 8))
(assert
(= #b01100100
(bvmul x y)))

(check-sat)
(exit)

Which version did you use?

Aina

> --
> You received this message because you are subscribed to the Google
> Groups "Boolector" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to boolector+...@googlegroups.com
> <mailto:boolector+...@googlegroups.com>.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/boolector/54832403-8d09-452b-b794-afe81fcd50f3%40googlegroups.com
> <https://groups.google.com/d/msgid/boolector/54832403-8d09-452b-b794-afe81fcd50f3%40googlegroups.com?utm_medium=email&utm_source=footer>.