active questions tagged z3 - Stack Overflow News Feed 
Saturday, August 01, 2015  |  From active questions tagged z3 - Stack Overflow




I am completely scratching my head over why I'm getting segmentation faults when I ask check-sat for (what I think is) a fairly simple bit of SMT2 code I'm trying to run in Z3.



(declare-const A Int)
(declare-const B Int)
(declare-const C Int)
(declare-const D Int)
(assert (= A (or 2 3 5 7)))
(define-fun W ((In1 Int)) Int
    (ite (= In1 2) (or 3 5) 
        (ite (= In1 3) (or 5 7) 
            (ite (= In1 5) 7 
                (ite (= In1 7) 3 11)
            )
        )
    )
)
(assert (= B (W A)))
(assert (= C (W B)))
(assert (= D (W C)))
(declare-const MULT Int)
(assert (= MULT (* A B C D)))

; 210 because 210 = 2*3*5*7

(declare-const MODULUS Int)
(assert (= 0 (rem MULT 210)))
(assert (= MODULUS 0))
(echo "Check 1")
(check-sat)
(echo "Check 2")
(get-model)


The model seems happy enough to return a non-numerical model if I remove the MODULUS bit of the code, but what I was expecting was a numerical solution where A=2, B=3, C=5, D=7 (and the MODULUS bit to work).



(model 
(define-fun D () Int
(let ((a!1 (ite (= (or 2 3 5 7) 5) 7 (ite (= (or 2 3 5 7) 7) 3 11))))
(let ((a!2 (ite (= (or 2 3 5 7) 2) (or 3 5)
(ite (= (or 2 3 5 7) 3) (or 5 7) a!1))))
(let ((a!3 (ite (= a!2 3) (or 5 7) (ite (= a!2 5) 7 (ite (= a!2 7) 3 11)))))
(let ((a!4 (ite (= (ite (= a!2 2) (or 3 5) a!3) 7) 3 11)))
(let ((a!5 (ite (= (ite (= a!2 2) (or 3 5) a!3) 5) 7 a!4)))
(let ((a!6 (ite (= (ite (= a!2 2) (or 3 5) a!3) 3) (or 5 7) a!5)))
(ite (= (ite (= a!2 2) (or 3 5) a!3) 2) (or 3 5) a!6))))))))

(define-fun C () Int
(let ((a!1 (ite (= (or 2 3 5 7) 5) 7 (ite (= (or 2 3 5 7) 7) 3 11))))
(let ((a!2 (ite (= (or 2 3 5 7) 2)(or 3 5)
(ite (= (or 2 3 5 7) 3) (or 5 7) a!1))))
(let ((a!3 (ite (= a!2 3) (or 5 7) (ite (= a!2 5) 7 (ite (= a!2 7) 3 11)))))
(ite (= a!2 2) (or 3 5) a!3)))))

(define-fun B () Int
(let ((a!1 (ite (= (or 2 3 5 7) 5) 7 (ite (= (or 2 3 5 7) 7) 3 11))))
(ite (= (or 2 3 5 7) 2) (or 3 5) (ite (= (or 2 3 5 7) 3) (or 5 7) a!1))))

(define-fun A () Int
(or 2 3 5 7))
)


I've tried using different solvers, and I've tried using Reals and I tried fiddling with the settings for model_evaluator and model but I'm really not sure what I'm doing....



Has anyone else had any similar difficulties or any luck better debugging a seg fault (segmentation fault: 11, if it helps?!), or am I going outside the limitations of Z3 here?



Many thanks



Thursday, July 30, 2015  |  From active questions tagged z3 - Stack Overflow




I am using Z3 version 4.4.0 on an Ubuntu 15.04 machine. The following model seems to cause a segmentation fault :



; mapping  
(declare-sort  Any   0 )
(declare-sort ProcBase 0)
(declare-fun Any_of_ProcBase ( ProcBase ) Any )
; Sort Real is default in smtlib 2.0. 
(declare-fun Any_of_Real ( Real ) Any )
(declare-fun execTime_of_ProcBase ( ProcBase ) Real )
(define-fun specA_of_ProcBase ( ( S ProcBase) ) Bool true ) 
(define-fun specG_of_ProcBase ( ( S ProcBase) ) Bool  ( not ( specA_of_ProcBase S ) ) )
(define-fun composedG_of_ProcBase ( ( S ProcBase ) ) Bool false  ) 
(define-fun composedA_of_ProcBase ( ( S ProcBase ) ) Bool true ) 
(declare-sort SwTask 0)
(declare-fun Any_of_SwTask ( SwTask ) Any )
(declare-fun requiredOps_of_SwTask ( SwTask ) Real )
(declare-fun desiredPeriod_of_SwTask ( SwTask ) Real )
(declare-fun complexity_of_SwTask ( SwTask ) Real )
(declare-fun execTime_of_SwTask ( SwTask ) Real )
(define-fun PeriodAssumption_of_SwTask ( (S SwTask) ) Bool ( and  ( >=  ( desiredPeriod_of_SwTask S  )  ( execTime_of_SwTask S  )  )  ( >=  ( complexity_of_SwTask S  )  ( to_real  0  )  )  )  )
(define-fun Ops_of_SwTask ( (S SwTask) ) Bool  ( =  ( requiredOps_of_SwTask S  )  ( complexity_of_SwTask S  )  )  )
(define-fun specA_of_SwTask ( ( S SwTask) ) Bool ( PeriodAssumption_of_SwTask S ) )
(define-fun specG_of_SwTask ( ( S SwTask) ) Bool ( or ( Ops_of_SwTask S ) ( not ( specA_of_SwTask S ) ) ) )
(define-fun composedG_of_SwTask ( ( S SwTask ) ) Bool false  ) 
(define-fun composedA_of_SwTask ( ( S SwTask ) ) Bool true ) 
(declare-sort Processor 0)
(declare-fun Any_of_Processor ( Processor ) Any )
(declare-fun ProcBase_of_Processor ( Processor ) ProcBase )
(declare-fun opsPerSec_of_Processor ( Processor ) Real )
(declare-fun requriedOps_of_Processor ( Processor ) Real )
(define-fun G_of_Processor ( (S Processor) ) Bool  ( =  ( execTime_of_ProcBase ( ProcBase_of_Processor S )   )  ( / ( requriedOps_of_Processor S  )  ( opsPerSec_of_Processor S  )  )  )  )
(define-fun specA_of_Processor ( ( S Processor) ) Bool true ) 
(define-fun specG_of_Processor ( ( S Processor) ) Bool ( or ( G_of_Processor S ) ( not ( specA_of_Processor S ) ) ) )
(define-fun composedG_of_Processor ( ( S Processor ) ) Bool false  ) 
(define-fun composedA_of_Processor ( ( S Processor ) ) Bool true ) 
(declare-sort Mapping 0)
(declare-fun Any_of_Mapping ( Mapping ) Any )
(declare-sort Array_t_SwTask_t 0)
(declare-fun Any_of_Array_t_SwTask_t ( Array_t_SwTask_t ) Any )
; Sort Int is default in smtlib 2.0. 
(declare-fun Any_of_Int ( Int ) Any )
(declare-fun select_of_Array_t_SwTask_t ( Array_t_SwTask_t Int ) SwTask )
(declare-fun size_of_Array_t_SwTask_t ( Array_t_SwTask_t ) Int )
(define-fun specA_of_Array_t_SwTask_t ( ( S Array_t_SwTask_t) ) Bool true ) 
(define-fun specG_of_Array_t_SwTask_t ( ( S Array_t_SwTask_t) ) Bool  ( not ( specA_of_Array_t_SwTask_t S ) ) )
(define-fun composedG_of_Array_t_SwTask_t ( ( S Array_t_SwTask_t ) ) Bool false  ) 
(define-fun composedA_of_Array_t_SwTask_t ( ( S Array_t_SwTask_t ) ) Bool true ) 
(declare-fun tasks_of_Mapping ( Mapping ) Array_t_SwTask_t )
(declare-sort Array_t_Processor_t 0)
(declare-fun Any_of_Array_t_Processor_t ( Array_t_Processor_t ) Any )
(declare-fun select_of_Array_t_Processor_t ( Array_t_Processor_t Int ) Processor )
(declare-fun size_of_Array_t_Processor_t ( Array_t_Processor_t ) Int )
(define-fun specA_of_Array_t_Processor_t ( ( S Array_t_Processor_t) ) Bool true ) 
(define-fun specG_of_Array_t_Processor_t ( ( S Array_t_Processor_t) ) Bool  ( not ( specA_of_Array_t_Processor_t S ) ) )
(define-fun composedG_of_Array_t_Processor_t ( ( S Array_t_Processor_t ) ) Bool false  ) 
(define-fun composedA_of_Array_t_Processor_t ( ( S Array_t_Processor_t ) ) Bool true ) 
(declare-fun procs_of_Mapping ( Mapping ) Array_t_Processor_t )
(declare-sort Array_t_Real_t 0)
(declare-fun Any_of_Array_t_Real_t ( Array_t_Real_t ) Any )
(declare-fun select_of_Array_t_Real_t ( Array_t_Real_t Int ) Real )
(declare-fun size_of_Array_t_Real_t ( Array_t_Real_t ) Int )
(define-fun specA_of_Array_t_Real_t ( ( S Array_t_Real_t) ) Bool true ) 
(define-fun specG_of_Array_t_Real_t ( ( S Array_t_Real_t) ) Bool  ( not ( specA_of_Array_t_Real_t S ) ) )
(define-fun composedG_of_Array_t_Real_t ( ( S Array_t_Real_t ) ) Bool false  ) 
(define-fun composedA_of_Array_t_Real_t ( ( S Array_t_Real_t ) ) Bool true ) 
(declare-sort Array_t_Array_t_Real_t_t 0)
(declare-fun Any_of_Array_t_Array_t_Real_t_t ( Array_t_Array_t_Real_t_t ) Any )
(declare-fun select_of_Array_t_Array_t_Real_t_t ( Array_t_Array_t_Real_t_t Int ) Array_t_Real_t )
(declare-fun size_of_Array_t_Array_t_Real_t_t ( Array_t_Array_t_Real_t_t ) Int )
(define-fun specA_of_Array_t_Array_t_Real_t_t ( ( S Array_t_Array_t_Real_t_t) ) Bool true ) 
(define-fun specG_of_Array_t_Array_t_Real_t_t ( ( S Array_t_Array_t_Real_t_t) ) Bool  ( not ( specA_of_Array_t_Array_t_Real_t_t S ) ) )
(define-fun composedG_of_Array_t_Array_t_Real_t_t ( ( S Array_t_Array_t_Real_t_t ) ) Bool false  ) 
(define-fun composedA_of_Array_t_Array_t_Real_t_t ( ( S Array_t_Array_t_Real_t_t ) ) Bool true ) 
(declare-fun requiredOps_of_Mapping ( Mapping ) Array_t_Array_t_Real_t_t )
(declare-fun mappedTo_of_Mapping (   SwTask Processor )  Bool  )
(define-fun MappingConstraints_of_Mapping ( (S Mapping) ) Bool ( and ( and  ( =  ( size_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )  )  ( size_of_Array_t_Processor_t ( procs_of_Mapping S )  )  ) ( and ( and ( and ( and ( and ( and ( and  ( =  ( size_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   )  ( size_of_Array_t_SwTask_t ( tasks_of_Mapping S )  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   -1   )  ( to_real  0  )  )  ) ( and ( and ( and  ( =>   ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   0  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   0  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   0   )  ( to_real  ( + ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   -1   )  ( requiredOps_of_SwTask ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   0  )   )  )  )  )  ) ( =>  ( not  ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   0  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   0  )  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   0   )  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   -1   )  )  )  ) ( and  ( =>   ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   1  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   0  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   1   )  ( to_real  ( + ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   0   )  ( requiredOps_of_SwTask ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   1  )   )  )  )  )  ) ( =>  ( not  ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   1  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   0  )  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   1   )  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   0   )  )  )  )  ) ( and  ( =>   ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   2  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   0  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   2   )  ( to_real  ( + ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   1   )  ( requiredOps_of_SwTask ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   2  )   )  )  )  )  ) ( =>  ( not  ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   2  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   0  )  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   2   )  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   1   )  )  )  )  )  )  ( =  ( requriedOps_of_Processor ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   0  )   )  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   0  )   ( - ( size_of_Array_t_SwTask_t ( tasks_of_Mapping S )  )  1  )   )  )  )  ( =  ( size_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   )  ( size_of_Array_t_SwTask_t ( tasks_of_Mapping S )  )  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   -1   )  ( to_real  0  )  )  ) ( and ( and ( and  ( =>   ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   0  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   1  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   0   )  ( to_real  ( + ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   -1   )  ( requiredOps_of_SwTask ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   0  )   )  )  )  )  ) ( =>  ( not  ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   0  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   1  )  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   0   )  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   -1   )  )  )  ) ( and  ( =>   ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   1  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   1  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   1   )  ( to_real  ( + ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   0   )  ( requiredOps_of_SwTask ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   1  )   )  )  )  )  ) ( =>  ( not  ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   1  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   1  )  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   1   )  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   0   )  )  )  )  ) ( and  ( =>   ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   2  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   1  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   2   )  ( to_real  ( + ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   1   )  ( requiredOps_of_SwTask ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   2  )   )  )  )  )  ) ( =>  ( not  ( mappedTo_of_Mapping S   ( select_of_Array_t_SwTask_t ( tasks_of_Mapping S )   2  )   ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   1  )  )  )  ( =  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   2   )  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   1   )  )  )  )  )  )  ( =  ( requriedOps_of_Processor ( select_of_Array_t_Processor_t ( procs_of_Mapping S )   1  )   )  ( select_of_Array_t_Real_t ( select_of_Array_t_Array_t_Real_t_t ( requiredOps_of_Mapping S )   1  )   ( - ( size_of_Array_t_SwTask_t ( tasks_of_Mapping S )  )  1  )   )  )  )  ) ( forall  ( ( sw SwTask ) ) ( exists  ( ( p Processor ) )  ( mappedTo_of_Mapping S   sw   p  )  )  )  )  )
(define-fun specA_of_Mapping ( ( S Mapping) ) Bool true ) 
(define-fun specG_of_Mapping ( ( S Mapping) ) Bool ( or ( MappingConstraints_of_Mapping S ) ( not ( specA_of_Mapping S ) ) ) )
(define-fun composedG_of_Mapping ( ( S Mapping ) ) Bool false  ) 
(define-fun composedA_of_Mapping ( ( S Mapping ) ) Bool true ) 
(declare-sort System 0)
(declare-fun Any_of_System ( System ) Any )
(declare-fun proc1_of_System ( System ) Processor )
(declare-fun proc2_of_System ( System ) Processor )
(declare-fun task1_of_System ( System ) SwTask )
(declare-fun task2_of_System ( System ) SwTask )
(declare-fun task3_of_System ( System ) SwTask )
(declare-fun mapping_of_System ( System ) Mapping )
(define-fun Conn_of_System ( (S System) ) Bool ( and ( and ( and ( and ( and ( and ( and ( and ( and ( and ( and ( and ( and ( and  ( =  ( select_of_Array_t_Processor_t ( procs_of_Mapping ( mapping_of_System S )  )   0   )  ( proc1_of_System S  )  )  ( =  ( select_of_Array_t_Processor_t ( procs_of_Mapping ( mapping_of_System S )  )   1   )  ( proc2_of_System S  )  )  )  ( =  ( select_of_Array_t_SwTask_t ( tasks_of_Mapping ( mapping_of_System S )  )   0   )  ( task1_of_System S  )  )  )  ( =  ( select_of_Array_t_SwTask_t ( tasks_of_Mapping ( mapping_of_System S )  )   1   )  ( task2_of_System S  )  )  )  ( =  ( select_of_Array_t_SwTask_t ( tasks_of_Mapping ( mapping_of_System S )  )   2   )  ( task3_of_System S  )  )  )  ( =  ( size_of_Array_t_Processor_t ( procs_of_Mapping ( mapping_of_System S )  )   )  2  )  )  ( =  ( size_of_Array_t_SwTask_t ( tasks_of_Mapping ( mapping_of_System S )  )   )  3  )  )  ( =  ( complexity_of_SwTask ( task1_of_System S )  )  ( to_real  100  )  )  )  ( =  ( complexity_of_SwTask ( task2_of_System S )  )  ( to_real  100  )  )  )  ( =  ( complexity_of_SwTask ( task3_of_System S )  )  ( to_real  100  )  )  )  ( =  ( opsPerSec_of_Processor ( proc1_of_System S )  )  ( to_real  200  )  )  )  ( =  ( opsPerSec_of_Processor ( proc2_of_System S )  )  ( to_real  200  )  )  )  ( =  ( desiredPeriod_of_SwTask ( task1_of_System S )  )  ( to_real  1  )  )  )  ( =  ( desiredPeriod_of_SwTask ( task2_of_System S )  )  ( to_real  1  )  )  )  ( =  ( desiredPeriod_of_SwTask ( task3_of_System S )  )  ( to_real  1  )  )  )  )
(define-fun specA_of_System ( ( S System) ) Bool true ) 
(define-fun specG_of_System ( ( S System) ) Bool  ( not ( specA_of_System S ) ) )
(define-fun composedG_of_System ( ( S System ) ) Bool ( and  true  ( Conn_of_System S ) ( => ( specA_of_Processor ( proc1_of_System S ) )( specG_of_Processor ( proc1_of_System S ) ) ) ( => ( specA_of_Processor ( proc2_of_System S ) )( specG_of_Processor ( proc2_of_System S ) ) ) ( => ( specA_of_SwTask ( task1_of_System S ) )( specG_of_SwTask ( task1_of_System S ) ) ) ( => ( specA_of_SwTask ( task2_of_System S ) )( specG_of_SwTask ( task2_of_System S ) ) ) ( => ( specA_of_SwTask ( task3_of_System S ) )( specG_of_SwTask ( task3_of_System S ) ) ) ( => ( specA_of_Mapping ( mapping_of_System S ) )( specG_of_Mapping ( mapping_of_System S ) ) )   ) ) 
(define-fun composedA_of_System ( ( S System ) ) Bool  ( or ( and  true  ( specA_of_Processor ( proc1_of_System S ) )( specA_of_Processor ( proc2_of_System S ) )( specA_of_SwTask ( task1_of_System S ) )( specA_of_SwTask ( task2_of_System S ) )( specA_of_SwTask ( task3_of_System S ) )( specA_of_Mapping ( mapping_of_System S ) ) ) (not  ( composedG_of_System S ) )  ) ) 
; check implementality for System
(declare-const S_System System )
(assert ( composedA_of_System  S_System ) )
(assert ( composedG_of_System  S_System ) )
(check-sat)


The problem seems to be caused by the function MappingConstraints_of_Mapping. If the sum operator in that function is removed by removing the second operand, then Z3 has no problem solving this instance.



Wednesday, July 29, 2015  |  From active questions tagged z3 - Stack Overflow




(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
(declare-const p1 (Pair Int Int))
(declare-const p2 (Pair Int Int))


I tried writing "mk-pair (first+second T1) (second T2)", but in practise it's the same as the first option. Does anyone know how to use a different constructor? Could someone give me an example? Thanks!



Friday, July 24, 2015  |  From active questions tagged z3 - Stack Overflow




How can I simplify the following expression using Z3 Solver?



(declare-const c0 Int)
(declare-const c1 Int)
(declare-const c2 Int)

(assert (let ((a!1 (to_real (+ (* (* 2 c0) c2)
                   (* (* 2 c0) c1)
                   (* 2 c1 c2)
                   (* c0 (- c0 1))
                   (* c1 (- c1 1))))))
  (let ((a!2 (/ (to_real (* (* 2 c0) c2)) a!1)))
  (and (or (and (<= c2 1) (>= c2 1) (<= c0 2) (>= c0 2) (<= c1 3) (>= c1 3))
           (and (<= c2 1) (>= c2 1) (<= c0 3) (>= c0 3) (<= c1 2) (>= c1 2)))
  (= (/ 2.0 15.0) a!2))))
)

(apply (then qe propagate-values (repeat (then ctx-solver-simplify propagate-ineqs) 10)))


Link : http://rise4fun.com/Z3/u7F7



I tried all the possible tactics that I know about and yet ended up causing time out by the solver. Is there a way that I can avoid time out? Is it suppose to return false as a result in Java API?



Friday, July 24, 2015  |  From active questions tagged z3 - Stack Overflow




I have just started playing with Z3 solver, after it was open sourced.



I am using Z3 as a command line black box tool at present, and would like it to dump counterexamples if the model is SAT. I am mostly passing QF_NIA and QF_LIA queries. I noticed that an option equivalent to CVC4s --dump-models doesn't exist in Z3. I could write (dump-model) after (check-sat) in the SMT2lib file, but that errors out if the formula is actually unsat.



The language of SMT2 lib though looks lispish, is far from being a properly interpreted interactive language. For example, something like (cond (check-sat) (dump-model)) should work.



In any case, being new to the Z3 source code, I've hacked up something, and thought I'd share it with the dev team. I have inlined a patch (not knowing how to attach stuff in stackoverflow), which if incorporated in the mainline, that would be great. Let me know if there is a better way of doing the same thing.



Also, apologies if this is not the right forum for this type of discussion. Please let me know then the correct avenue.



I also have some Z3 performance related questions on seemingly simple queries, which CVC4 is able to solve easily, that I'll reserve for the future discussion.



Thanks,



Pankaj



Patch begins:



diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp                                                  
index 7316085..c45f668 100644                                   
--- a/src/cmd_context/cmd_context.cpp                           
+++ b/src/cmd_context/cmd_context.cpp                           
@@ -40,6 +40,8 @@ Notes:                                        
 #include"scoped_timer.h"                                       
 #include"interpolant_cmds.h"                                   

+extern bool g_get_model_when_sat;                              
+                                                               
 func_decls::func_decls(ast_manager & m, func_decl * f):        
     m_decls(TAG(func_decl*, f, 0)) {                           
     m.inc_ref(f);                                              
@@ -1355,8 +1357,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions                         
         m_solver->set_status(r);                               
         display_sat_result(r);                                 
         validate_check_sat_result(r);                          
-        if (r == l_true)                                       
+        if (r == l_true) {                                     
             validate_model();                                  
+            if (g_get_model_when_sat) {                        
+                symbol gm("get-model");                        
+                cmd *gm_cmd = find_cmd(gm);                    
+                gm_cmd->prepare(*this);                        
+                gm_cmd->execute(*this);                        
+            }                                                  
+        }                                                      
     }                                                          
     else {                                                     
         // There is no solver installed in the command context.
diff --git a/src/shell/main.cpp b/src/shell/main.cpp            
index 0eb612f..2fbd8ec 100644                                   
--- a/src/shell/main.cpp                                        
+++ b/src/shell/main.cpp                                        
@@ -43,6 +43,7 @@ bool                g_standard_input      = false;                                                            
 input_kind          g_input_kind          = IN_UNSPECIFIED;    
 bool                g_display_statistics  = false;             
 bool                g_display_istatistics = false;             
+bool                g_get_model_when_sat  = false;             

 void error(const char * msg) {                                 
     std::cerr << "Error: " << msg << "\n";                     
@@ -92,6 +93,7 @@ void display_usage() {
     //
     std::cout << "\nOutput:\n";
     std::cout << "  -st         display statistics.\n";
+    std::cout << "  -m          Execute get-model after every check-sat, if model is available\n";
 #if defined(Z3DEBUG) || defined(_TRACE)
     std::cout << "\nDebugging support:\n";
 #endif
@@ -174,6 +176,9 @@ void parse_cmd_line_args(int argc, char ** argv) {
             else if (strcmp(opt_name, "st") == 0) {
                 g_display_statistics = true;
             }
+            else if (strcmp(opt_name, "m") == 0) {
+                g_get_model_when_sat = true;
+            }
             else if (strcmp(opt_name, "ist") == 0) {
                 g_display_istatistics = true;
             }


Patch ends



Friday, July 24, 2015  |  From active questions tagged z3 - Stack Overflow




My scenario is as follows:



  • First I follow the optimistic assumptions that all is well; so I check the assertions without asking for an unsat core (just using Assert).
  • When I however get status UNSATISFIABLE during one of the tests I change the strategy and use AssertAndTrack from the very beginning to get the full unsat core.

With version 4.3.2 this works perfectly, but after switching to 4.4 (stable and latest) Z3 often returns status UNKNOWN (even for checks which delivered SATISFIABLE in 4.4 without AssertAndTrack).



Does anybody can give me a hint how to solve the problem or what to do to further analyze the problem?



Thanks



Christian



Thursday, July 23, 2015  |  From active questions tagged z3 - Stack Overflow




I have a project that generated big smtlib2 problems as strings and it solved them by writing the problems to a file and then calling a solver via exec(). I'm trying to integrate Z3 to solve it via API, because the problem is inherently incremental, and thus the learning by the solver will be used between calls.



The problems I face are:



  1. I get a segfault when I assert something using the function
    'z3_assert_str' shown below.
  2. The trace file is always empty, it seems the config parameters are not working or not corretly set.

I have tried with Z3 4.4.0 and trunk, directly from github.



What am I doing wrong?






Here are the important bits from the class:


foo.h



In this class I maintain two vectors (v_symbols and v_func_decl) to keep track of what I have inserted in the problem, so then I can call "Z3_parse_smtlib2_string"



// attributes of foo.h
z3::config * cfg;
z3::context * c;
z3::solver * s;

std::vector<Z3_symbol> v_symbols;
std::vector<Z3_func_decl> v_func_decl;

// main z3 interaction function
void z3_assert_str(std::string s);

foo.cpp



// in the class constructor, I initialize the 
// z3 structures as follows
cfg = new z3::config(); 
cfg->set("trace", true);
cfg->set("trace_file_name", "z3.log");
c = new z3::context(*cfg);
s = new z3::solver(*c);

// then I keep adding integer vars
expr foobar = c->int_const(obj.c_str());
v_symbols.push_back(foobar.decl().name());
v_func_decl.push_back(foobar.decl());  

// and Uninterpreted Functions (UF)
func_decl f = c->function(f_name.c_str(), sort_vec, z3_int_sort);
v_symbols.push_back(f.name());
v_func_decl.push_back(f);

// and finally the funcion that asserts a smtlib2 string
void encodingUFVisitorZ3::z3_assert_str(std::string constraint) {
    try {
        Z3_ast ast = Z3_parse_smtlib2_string(*c,constraint.c_str(),
                0, 0, 0,
                v_symbols.size(),
                &v_symbols[0],
                &v_func_decl[0]);

        z3::expr constr = to_expr(*c, ast);
        s->add(constr);
    } catch (z3::exception ex) {
        std::cout << "failed: " << ex << "\n";
    }
}

segfault



Program received signal SIGSEGV, Segmentation fault.
0x00007ffff6c865e6 in func_decl_info::is_right_associative (this=0x2) at ../src/ast/ast.h:372
372     bool is_right_associative() const { return m_right_assoc; }
(gdb) bt
#0  0x00007ffff6c865e6 in func_decl_info::is_right_associative (this=0x2) at ../src/ast/ast.h:372
#1  0x00007ffff730d7b5 in func_decl::is_right_associative (this=0xa623d8) at ../src/ast/ast.h:591
#2  0x00007ffff730375b in ast_manager::mk_app (this=0x8a4058, decl=0xa623d8, num_args=2, args=0xa6d9a0) at ../src/ast/ast.cpp:2046
#3  0x00007ffff703da03 in cmd_context::mk_app (this=0x7fffffffd2e0, s=..., num_args=2, args=0xa6d9a0, num_indices=0, indices=0x0, range=0x0, result=...) at ../src/cmd_context/cmd_context.cpp:998
#4  0x00007ffff701cfb3 in smt2::parser::pop_app_frame (this=0x7fffffffca80, fr=0x8c1bc0) at ../src/parsers/smt2/smt2parser.cpp:1526
#5  0x00007ffff701eafc in smt2::parser::pop_expr_frame (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1663
#6  0x00007ffff701edd3 in smt2::parser::parse_expr (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1696
#7  0x00007ffff7020910 in smt2::parser::parse_assert (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1957
#8  0x00007ffff7022ca5 in smt2::parser::parse_cmd (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:2319
#9  0x00007ffff7023cb6 in smt2::parser::operator() (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:2470
#10 0x00007ffff7012df1 in parse_smt2_commands (ctx=..., is=..., interactive=false, ps=...) at ../src/parsers/smt2/smt2parser.cpp:2519
#11 0x00007ffff68de38b in parse_smtlib2_stream (exec=false, c=0x8a3148, is=..., num_sorts=0, sort_names=0x0, sorts=0x0, num_decls=31, decl_names=0xa62570, decls=0xa62680) at ../src/api/api_parsers.cpp:272
#12 0x00007ffff68de664 in Z3_parse_smtlib2_string (c=0x8a3148, str=0xa63758 "(assert (= (at plane1 0) city1))", num_sorts=0, sort_names=0x0, sorts=0x0, num_decls=31, decl_names=0xa62570, decls=0xa62680) at ../src/api/api_parsers.cpp:294
#13 0x0000000000529e38 in encodingUFVisitorZ3::z3_assert_str (this=0x8a2220, constraint=...) at encodingUFVisitorZ3.cpp:308
#14 0x0000000000527f4b in encodingUFVisitorZ3::assertInitialState (this=0x8a2220) at encodingUFVisitorZ3.cpp:118
#15 0x000000000052977d in encodingUFVisitorZ3::solve (this=0x8a2220) at encodingUFVisitorZ3.cpp:238
#16 0x0000000000479854 in PDDLProblem::solve (this=0x84c590) at PDDLProblem.cpp:687
#17 0x000000000053afd1 in main (argc=9, argv=0x7fffffffe018) at main.cpp:203


Thursday, July 23, 2015  |  From active questions tagged z3 - Stack Overflow




I am using z3 as the underlying constraint solver in my application through its C++ interface. I declare an z3 context as member of a class which is used to solve many independent constraint sets.



Here is the thing: I declare the z3 'solver' when solving a constraint set but the z3 'context' is the same one during the solving of many independent problems.
I'm not sure whether it's correct to use the same z3 context during solving of independent problems. BTW my program does what I expected.



Thursday, July 23, 2015  |  From active questions tagged z3 - Stack Overflow




I need write a matrix[n][n] in smt to using in Z3opt.
but, in rise4fun Guide i did not find.
I use Z3opt site to write my code.
i can't use c/c++/.net, only smt.
thanks in advanced.



Wednesday, July 22, 2015  |  From active questions tagged z3 - Stack Overflow




My scenario is as follows:



  • First I follow the optimistic assumptions that all is well; so I check the assertions without asking for an unsat core (just using Assert).
  • When I however get status UNSATISFIABLE during one of the tests I change the strategy and use AssertAndTrack from the very beginning to get the full unsat core.

With version 4.3.2 this works perfectly, but after switching to 4.4 (stable and latest) Z3 often returns status UNKNOWN (even for checks which delivered SATISFIABLE in 4.4 without AssertAndTrack).



Does anybody can give me a hint how to solve the problem or what to do to further analyze the problem?



Thanks



Christian



Wednesday, July 22, 2015  |  From active questions tagged z3 - Stack Overflow




My scenario is as follows:



  • First I follow the optimistic assumptions that all is well; so I check the assertions without asking for an unsat core (just using Assert).
  • When I however get status UNSATISFIABLE during one of the tests I change the strategy and use AssertAndTrack from the very beginning to get the full unsat core.

With version 4.3.2 this works perfectly, but after switching to 4.4 (stable and latest) Z3 often returns status UNKNOWN (even for checks which delivered SATISFIABLE in 4.4 without AssertAndTrack).



Does anybody can give me a hint how to solve the problem or what to do to further analyze the problem?



Thanks



Christian



Tuesday, July 21, 2015  |  From active questions tagged z3 - Stack Overflow




I have a project that generated big smtlib2 problems as strings and it solved them by writing the problems to a file and then calling a solver via exec(). I'm trying to integrate Z3 to solve it via API, because the problem is inherently incremental, and thus the learning by the solver will be used between calls.



The problems I face are:



  1. I get a segfault when I assert something using the function
    'z3_assert_str' shown below.
  2. The trace file is always empty, it seems the config parameters are not working or not corretly set.

I have tried with Z3 4.4.0 and trunk, directly from github.



What am I doing wrong?






Here are the important bits from the class:


foo.h



In this class I maintain two vectors (v_symbols and v_func_decl) to keep track of what I have inserted in the problem, so then I can call "Z3_parse_smtlib2_string"



// attributes of foo.h
z3::config * cfg;
z3::context * c;
z3::solver * s;

std::vector<Z3_symbol> v_symbols;
std::vector<Z3_func_decl> v_func_decl;

// main z3 interaction function
void z3_assert_str(std::string s);

foo.cpp



// in the class constructor, I initialize the 
// z3 structures as follows
cfg = new z3::config(); 
cfg->set("trace", true);
cfg->set("trace_file_name", "z3.log");
c = new z3::context(*cfg);
s = new z3::solver(*c);

// then I keep adding integer vars
expr foobar = c->int_const(obj.c_str());
v_symbols.push_back(foobar.decl().name());
v_func_decl.push_back(foobar.decl());  

// and Uninterpreted Functions (UF)
func_decl f = c->function(f_name.c_str(), sort_vec, z3_int_sort);
v_symbols.push_back(f.name());
v_func_decl.push_back(f);

// and finally the funcion that asserts a smtlib2 string
void encodingUFVisitorZ3::z3_assert_str(std::string constraint) {
    try {
        Z3_ast ast = Z3_parse_smtlib2_string(*c,constraint.c_str(),
                0, 0, 0,
                v_symbols.size(),
                &v_symbols[0],
                &v_func_decl[0]);

        z3::expr constr = to_expr(*c, ast);
        s->add(constr);
    } catch (z3::exception ex) {
        std::cout << "failed: " << ex << "\n";
    }
}

segfault



Program received signal SIGSEGV, Segmentation fault.
0x00007ffff6c865e6 in func_decl_info::is_right_associative (this=0x2) at ../src/ast/ast.h:372
372     bool is_right_associative() const { return m_right_assoc; }
(gdb) bt
#0  0x00007ffff6c865e6 in func_decl_info::is_right_associative (this=0x2) at ../src/ast/ast.h:372
#1  0x00007ffff730d7b5 in func_decl::is_right_associative (this=0xa623d8) at ../src/ast/ast.h:591
#2  0x00007ffff730375b in ast_manager::mk_app (this=0x8a4058, decl=0xa623d8, num_args=2, args=0xa6d9a0) at ../src/ast/ast.cpp:2046
#3  0x00007ffff703da03 in cmd_context::mk_app (this=0x7fffffffd2e0, s=..., num_args=2, args=0xa6d9a0, num_indices=0, indices=0x0, range=0x0, result=...) at ../src/cmd_context/cmd_context.cpp:998
#4  0x00007ffff701cfb3 in smt2::parser::pop_app_frame (this=0x7fffffffca80, fr=0x8c1bc0) at ../src/parsers/smt2/smt2parser.cpp:1526
#5  0x00007ffff701eafc in smt2::parser::pop_expr_frame (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1663
#6  0x00007ffff701edd3 in smt2::parser::parse_expr (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1696
#7  0x00007ffff7020910 in smt2::parser::parse_assert (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:1957
#8  0x00007ffff7022ca5 in smt2::parser::parse_cmd (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:2319
#9  0x00007ffff7023cb6 in smt2::parser::operator() (this=0x7fffffffca80) at ../src/parsers/smt2/smt2parser.cpp:2470
#10 0x00007ffff7012df1 in parse_smt2_commands (ctx=..., is=..., interactive=false, ps=...) at ../src/parsers/smt2/smt2parser.cpp:2519
#11 0x00007ffff68de38b in parse_smtlib2_stream (exec=false, c=0x8a3148, is=..., num_sorts=0, sort_names=0x0, sorts=0x0, num_decls=31, decl_names=0xa62570, decls=0xa62680) at ../src/api/api_parsers.cpp:272
#12 0x00007ffff68de664 in Z3_parse_smtlib2_string (c=0x8a3148, str=0xa63758 "(assert (= (at plane1 0) city1))", num_sorts=0, sort_names=0x0, sorts=0x0, num_decls=31, decl_names=0xa62570, decls=0xa62680) at ../src/api/api_parsers.cpp:294
#13 0x0000000000529e38 in encodingUFVisitorZ3::z3_assert_str (this=0x8a2220, constraint=...) at encodingUFVisitorZ3.cpp:308
#14 0x0000000000527f4b in encodingUFVisitorZ3::assertInitialState (this=0x8a2220) at encodingUFVisitorZ3.cpp:118
#15 0x000000000052977d in encodingUFVisitorZ3::solve (this=0x8a2220) at encodingUFVisitorZ3.cpp:238
#16 0x0000000000479854 in PDDLProblem::solve (this=0x84c590) at PDDLProblem.cpp:687
#17 0x000000000053afd1 in main (argc=9, argv=0x7fffffffe018) at main.cpp:203


Tuesday, July 21, 2015  |  From active questions tagged z3 - Stack Overflow




Good day, auto deduction and verification hackers!



In order to gain a deeper understanding of how exactly WhyML provides proofs for ACSL-annotated C programs I am trying to manually "reproduce" the job Why3 does with WhyML program while translating it into SMT logic and feeding it into Z3 prover.



Lets say we have the following C fragment:



const int L = 3;
int a[L] = {0};
int i = 0;
while (i < L) {
  a[i] = i;
  i++;
}
assert (a[1] == 1);


I am trying to encode it into SMT logic like this:



(set-logic AUFNIRA)
(define-sort _array () (Array Int Int))
(declare-const ar _array)
(declare-fun set_a_i (_array Int Int) _array)
(assert (forall ((ar0 _array) (i Int) (j Int)) 
    (ite (< i j)   
                 (= (set_a_i ar0 i j) 
                    (set_a_i (store ar0 i i) (+ i 1) j))
                 (= (set_a_i ar0 i i) ar0) ))) 

(assert (= (select (set_a_i ar 0 3) 1) 1))
(check-sat)


Z3 gives "unknown".



This is probably because of quantification used in specifing set_a_i function. But I see no other ways to specify it.



I am aware of the following statements:



  • SMT solvers in general are not able to (or do it in a bad way) handle quantifications over arrays.
  • WhyML is able to prove such programs if I supply pre & post condition and loop invariant.
  • WhyML is able to prove such programs even when backend is set to Z3, so SMT solver itself is not an issue.
  • WhyML can produce z3 smt file, but to understand it is a great toil partly because of the automatic nature of whyML->smt translation (it doest not preserve variable names for example)

I read nearly all supplied materials for WhyML, Frama-C WP plugin and Z3. I also read several papers on verifing C code but found nothing regarding C --> SMT translation techniques.



Which materials should I study to gain this understanding? Could you please provide insights and/or links to papers describing this machinery of translating imperative code into multi-sorted first order logic.



I will appreciate any comments. Thanks!



Good luck,
Evgeniy.



Tuesday, July 21, 2015  |  From active questions tagged z3 - Stack Overflow




I have just started playing with Z3 solver, after it was open sourced.



I am using Z3 as a command line black box tool at present, and would like it to dump counterexamples if the model is SAT. I am mostly passing QF_NIA and QF_LIA queries. I noticed that an option equivalent to CVC4s --dump-models doesn't exist in Z3. I could write (dump-model) after (check-sat) in the SMT2lib file, but that errors out if the formula is actually unsat.



The language of SMT2 lib though looks lispish, is far from being a properly interpreted interactive language. For example, something like (cond (check-sat) (dump-model)) should work.



In any case, being new to the Z3 source code, I've hacked up something, and thought I'd share it with the dev team. I have inlined a patch (not knowing how to attach stuff in stackoverflow), which if incorporated in the mainline, that would be great. Let me know if there is a better way of doing the same thing.



Also, apologies if this is not the right forum for this type of discussion. Please let me know then the correct avenue.



I also have some Z3 performance related questions on seemingly simple queries, which CVC4 is able to solve easily, that I'll reserve for the future discussion.



Thanks,



Pankaj



Patch begins:



diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp                                                  
index 7316085..c45f668 100644                                   
--- a/src/cmd_context/cmd_context.cpp                           
+++ b/src/cmd_context/cmd_context.cpp                           
@@ -40,6 +40,8 @@ Notes:                                        
 #include"scoped_timer.h"                                       
 #include"interpolant_cmds.h"                                   

+extern bool g_get_model_when_sat;                              
+                                                               
 func_decls::func_decls(ast_manager & m, func_decl * f):        
     m_decls(TAG(func_decl*, f, 0)) {                           
     m.inc_ref(f);                                              
@@ -1355,8 +1357,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions                         
         m_solver->set_status(r);                               
         display_sat_result(r);                                 
         validate_check_sat_result(r);                          
-        if (r == l_true)                                       
+        if (r == l_true) {                                     
             validate_model();                                  
+            if (g_get_model_when_sat) {                        
+                symbol gm("get-model");                        
+                cmd *gm_cmd = find_cmd(gm);                    
+                gm_cmd->prepare(*this);                        
+                gm_cmd->execute(*this);                        
+            }                                                  
+        }                                                      
     }                                                          
     else {                                                     
         // There is no solver installed in the command context.
diff --git a/src/shell/main.cpp b/src/shell/main.cpp            
index 0eb612f..2fbd8ec 100644                                   
--- a/src/shell/main.cpp                                        
+++ b/src/shell/main.cpp                                        
@@ -43,6 +43,7 @@ bool                g_standard_input      = false;                                                            
 input_kind          g_input_kind          = IN_UNSPECIFIED;    
 bool                g_display_statistics  = false;             
 bool                g_display_istatistics = false;             
+bool                g_get_model_when_sat  = false;             

 void error(const char * msg) {                                 
     std::cerr << "Error: " << msg << "\n";                     
@@ -92,6 +93,7 @@ void display_usage() {
     //
     std::cout << "\nOutput:\n";
     std::cout << "  -st         display statistics.\n";
+    std::cout << "  -m          Execute get-model after every check-sat, if model is available\n";
 #if defined(Z3DEBUG) || defined(_TRACE)
     std::cout << "\nDebugging support:\n";
 #endif
@@ -174,6 +176,9 @@ void parse_cmd_line_args(int argc, char ** argv) {
             else if (strcmp(opt_name, "st") == 0) {
                 g_display_statistics = true;
             }
+            else if (strcmp(opt_name, "m") == 0) {
+                g_get_model_when_sat = true;
+            }
             else if (strcmp(opt_name, "ist") == 0) {
                 g_display_istatistics = true;
             }


Patch ends



Tuesday, July 21, 2015  |  From active questions tagged z3 - Stack Overflow




I am facing problem implementing verilog if condition in z3.



if(reset == 1){
  G5 <= 0;
} else {
  G5 <= G10;
}


I am trying to implement above code using ofollowing code in z3 smt.



s.add( (BoolExpr) ctx.mkITE( ctx.mkEq(reset,ctx.mkNumeral("1",ctx.mkBitVecSort(1))) , ctx.mkEq(G5,ctx.mkNumeral("0",ctx.mkBitVecSort(1))) , ctx.mkEq(G5,G10) ));
s.add( ctx.mkEq(reset,ctx.mkNumeral("1",ctx.mkBitVecSort(1))) );


While executing above step i am not able to control reset( i want G5<=G10 as solution). For example if i am trying to give reset as '0' for execution i am getting error as "invalid usage". because i am trying to constraint reset twice.



Please help me with above issue.



Tuesday, July 21, 2015  |  From active questions tagged z3 - Stack Overflow




I am experimenting with OpenJML in combination with Z3, and I'm trying to reason about double or float values:



class Test {

  //@ requires b > 0;
  void a(double b) {
  }

  void b() {
    a(2.4);
  }
}


I have already found out OpenJML uses AUFLIA as the default logic, which doesn't support reals. I am now using AUFNIRA.



Unfortunately, the tool is unable to prove this class:



→ java -jar openjml.jar -esc -prover z3_4_3 -exec ./z3 Test.java -noInternalSpecs -logic AUFNIRA

Test.java:8: warning: The prover cannot establish an assertion (Precondition: Test.java:3: ) in method b
    a(2.4);
     ^
Test.java:3: warning: Associated declaration: Test.java:8: 
  //@ requires b > 0;
      ^
2 warnings


Why is this?



Monday, July 20, 2015  |  From active questions tagged z3 - Stack Overflow




Suppose we have the following C annotated code:



#define L  3
int a[L] = {0};
/*@ requires \valid(a+(0..(L - 1)));
    ensures \forall int j; 0 <= j < L ==> (a[j] == j); */
int main() {
        int i = 0;
        /*@ loop assigns i, a[0..(i-1)];
            loop invariant inv1: 0 <= i <= L;
            loop invariant inv2:
                        \forall int k; 0 <= k < i ==> a[k] == k; 
        */
        while (i < L) {
          a[i] = i;
          i++;
        }
        /*@ assert final_progress:
               \forall int k; 0 < k < L ==> a[k] == a[k-1] + 1; 
            assert final_c: 
               a[2] == a[1] - 1; */
        return 0;
}


Why Alt-Ergo/Z3 yields "unknown" or timeouts for final_c assertion despite the fact that final_progress statement was proven?
I would definitely like to see "Not valid" for such obviously (from user point of view) invalid statements.



$ frama-c -wp -wp-rte -wp-prover z3 test2.c
..
[wp] [z3] Goal typed_main_assert_final_c : Unknown (455ms)

$ frama-c -wp -wp-rte -wp-prover alt-ergo test2.c 
..
[wp] [Alt-Ergo] Goal typed_main_assert_final_c : Timeout


Monday, July 20, 2015  |  From active questions tagged z3 - Stack Overflow




I ran the below code in z3 (java api):



BitVecExpr a = ctx.mkBVConst("a",8);
BitVecExpr b = ctx.mkBVConst("b",8);
BitVecExpr c = ctx.mkBVConst("c",8);
BitVecExpr d = (BitVecNum) ctx.mkNumeral("11",ctx.mkBitVecSort(8));
Solver s = ctx.mkSolver();
s.add(ctx.mkEq(c,ctx.mkBVXOR(a,b)));
s.add(ctx.mkEq(c,d));   
Model m = s.getModel();
System.out.println("m.eval(a) " + m.eval(a,false)); /*m.eval(a) 0 */
System.out.println("m.eval(b) " + m.eval(b,false));  /*m.eval(b) 11 */
System.out.println("m.eval(c) " + m.eval(c,false));  /*m.eval(c) 11 */


My questions are:



  1. How to pass a hexadecimal value for d? Does it only take a decimal value?

  2. Is there any other way to pass bit value to d?


Monday, July 20, 2015  |  From active questions tagged z3 - Stack Overflow




I need write a matrix[n][n] in smt to using in Z3opt.
but, in rise4fun Guide i did not find.
I use Z3opt site to write my code.
i can't use c/c++/.net, only smt.
thanks in advanced.



Monday, July 20, 2015  |  From active questions tagged z3 - Stack Overflow




I ran the below code in z3 (java api):



BitVecExpr a = ctx.mkBVConst("a",8);
BitVecExpr b = ctx.mkBVConst("b",8);
BitVecExpr c = ctx.mkBVConst("c",8);
BitVecExpr d = (BitVecNum) ctx.mkNumeral("11",ctx.mkBitVecSort(8));
Solver s = ctx.mkSolver();
s.add(ctx.mkEq(c,ctx.mkBVXOR(a,b)));
s.add(ctx.mkEq(c,d));   
Model m = s.getModel();
System.out.println("m.eval(a) " + m.eval(a,false)); /*m.eval(a) 0 */
System.out.println("m.eval(b) " + m.eval(b,false));  /*m.eval(b) 11 */
System.out.println("m.eval(c) " + m.eval(c,false));  /*m.eval(c) 11 */


My questions are:



  1. How to pass a hexadecimal value for d? Does it only take a decimal value?

  2. Is there any other way to pass bit value to d?


 active questions tagged z3 - Stack Overflow News Feed 

Last edited Nov 23, 2012 at 4:52 AM by leodemoura, version 13

Comments

No comments yet.