Le 18/03/2020 à 10:48, Julia Lawall a écrit : > When I run cvc4 on the command line, it ends with > > (error "Can't get-info :reason-unknown when the last result wasn't > unknown!") > > If I remove (get-info :reason-unknown) it ends with unsat (which is not > what I hoped for, but perhaps I am somehow not running it properly).
If your goal in Why3 is valid, then its negation is expected to be unsat on the SMT side. So, unless your goal was meant to be unprovable, this is fine. > But the unconditional (get-info :reason-unknown) doesn't look ideal. Agreed. Unfortunately, to make it conditional, Why3 would have to interact with the SMT solvers, that is, write on stdin, read on stdout, write on stdin, read on stdout, and so on. That is completely different from Why3's current architecture, which gives an input file to the SMT solver, wait for termination, then read stdout. Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
