cannot generate .smt2 file

[rachelwang]

For some reason, dReach cannot generate the .smt2 file for the following .drh file.

[10, 30.0] x; 
[0, 3] time;

{ mode 1;

  invt:
        (x >= 20);
  flow:
        d/dt[x] = 0 - 0.1 * x;
  jump:
        (x < 20) ==> @2 (x’ = x);
}
{ mode 2;

  invt:
        (x <= 22);
  flow:
        d/dt[x] = 5 - 0.1 * x;
  jump:
        (x > 22) ==> @1 (x' = x);
}
init:
@1  (x = 20);

goal:
@1  (x <= 22);

[rachelwang]

Follow-up:

The lack of "[0, 3] time;" is not the reason.

I have added "[0, 3] time;", but still cannot get the .smt2 file

[soonhokong]

It's because you have "’" instead of "'" at

  jump:
        (x < 20) ==> @2 (x’ = x);

It has to be

  jump:
        (x < 20) ==> @2 (x' = x);

[soonhokong]

BTW, @rachelwang, you can use the code-block feature of github markdown. Please read

https://help.github.com/articles/github-flavored-markdown#syntax-highlighting

[rachelwang]

This is weird as I copied that part directly from a runnable .drh file...

Anyway, thx

[soonhokong]

It's interesting that the second jump had the right symbol (')..

[rachelwang]

I finally find the reason of this automatic change.

Whenever you insert sth. before "'", it will change to "’" automatically...

On Tue, Apr 15, 2014 at 4:59 PM, Soonho Kong notifications@github.comwrote:

It's interesting that the second jump had the right symbol (')..

— Reply to this email directly or view it on GitHubhttps://github.com/dreal/dreal/issues/3#issuecomment-40533557 .

Ph.D. student Computer Science Department School of Computing Sciences Carnegie Mellon University

[soonhokong]

@rachelwang, It's because you're using OSX's TextEdit.App which has a feature called "smart quote" which does the job for you. You can disable it from the preference which you can go by cmd + ,.

Of course, I recommend you to use either vim or emacs.

[rachelwang]

Oh, really! I have to know more about Mac OSX from you, as I am new to it... Thx

On Tue, Apr 15, 2014 at 8:51 PM, Soonho Kong notifications@github.comwrote:

@rachelwang https://github.com/rachelwang, It's because you're using OSX's TextEdit.App which has a feature called "smart quote" which does the job for you. You can disable it from the preference which you can go by cmd

• ,.

Of course, I recommend you to use either vim1https://code.google.com/p/macvim/or emacs 2 http://emacsformacosx.com/.

— Reply to this email directly or view it on GitHubhttps://github.com/dreal/dreal/issues/3#issuecomment-40552105 .

Ph.D. student Computer Science Department School of Computing Sciences Carnegie Mellon University